[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A ∈ unitaryGroup n α ↔ A * star A = 1
[PROOFSTEP]
refine' ⟨And.right, fun hA => ⟨_, hA⟩⟩
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A * star A = 1
⊢ star A * A = 1
[PROOFSTEP]
simpa only [mul_eq_one_comm] using hA
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A ∈ unitaryGroup n α ↔ star A * A = 1
[PROOFSTEP]
refine' ⟨And.left, fun hA => ⟨hA, _⟩⟩
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : star A * A = 1
⊢ A * star A = 1
[PROOFSTEP]
rwa [mul_eq_one_comm] at hA 
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ det A ∈ unitary α
[PROOFSTEP]
constructor
[GOAL]
case left
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ star (det A) * det A = 1
[PROOFSTEP]
simpa [star, det_transpose] using congr_arg det hA.1
[GOAL]
case right
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ det A * star (det A) = 1
[PROOFSTEP]
simpa [star, det_transpose] using congr_arg det hA.2
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : { x // x ∈ unitaryGroup n α }
src✝ : (fun x => (n → α) →ₗ[α] n → α) ↑A := ↑Matrix.toLin' ↑A
x : n → α
⊢ ↑(comp (toLin' A⁻¹) (toLin' A)) x = ↑(toLin' (A⁻¹ * A)) x
[PROOFSTEP]
rw [← toLin'_mul]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : { x // x ∈ unitaryGroup n α }
src✝ : (fun x => (n → α) →ₗ[α] n → α) ↑A := ↑Matrix.toLin' ↑A
x : n → α
⊢ ↑(toLin' (A⁻¹ * A)) x = x
[PROOFSTEP]
rw [mul_left_inv, toLin'_one, id_apply]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : { x // x ∈ unitaryGroup n α }
src✝ : (fun x => (n → α) →ₗ[α] n → α) ↑A := ↑Matrix.toLin' ↑A
x : n → α
⊢ ↑(comp (toLin' A) (toLin' A⁻¹)) x = ↑(toLin' (A * A⁻¹)) x
[PROOFSTEP]
rw [← toLin'_mul]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : { x // x ∈ unitaryGroup n α }
src✝ : (fun x => (n → α) →ₗ[α] n → α) ↑A := ↑Matrix.toLin' ↑A
x : n → α
⊢ ↑(toLin' (A * A⁻¹)) x = x
[PROOFSTEP]
rw [mul_right_inv, toLin'_one, id_apply]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ ↑(toGL 1) = ↑1
[PROOFSTEP]
simp only [coe_toGL, toLin'_one]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ LinearMap.id = ↑1
[PROOFSTEP]
rfl
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A B : { x // x ∈ unitaryGroup n α }
⊢ ↑(toGL (A * B)) = ↑(toGL A * toGL B)
[PROOFSTEP]
simp only [coe_toGL, toLin'_mul]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A B : { x // x ∈ unitaryGroup n α }
⊢ comp (toLin' A) (toLin' B) = ↑(toGL A * toGL B)
[PROOFSTEP]
rfl
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
α : Type v
inst✝² : CommRing α
inst✝¹ : StarRing α
A✝ : Matrix n n α
β : Type v
inst✝ : CommRing β
A : Matrix n n β
⊢ A ∈ orthogonalGroup n β ↔ A * star A = 1
[PROOFSTEP]
refine' ⟨And.right, fun hA => ⟨_, hA⟩⟩
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
α : Type v
inst✝² : CommRing α
inst✝¹ : StarRing α
A✝ : Matrix n n α
β : Type v
inst✝ : CommRing β
A : Matrix n n β
hA : A * star A = 1
⊢ star A * A = 1
[PROOFSTEP]
simpa only [mul_eq_one_comm] using hA
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
α : Type v
inst✝² : CommRing α
inst✝¹ : StarRing α
A✝ : Matrix n n α
β : Type v
inst✝ : CommRing β
A : Matrix n n β
⊢ A ∈ orthogonalGroup n β ↔ star A * A = 1
[PROOFSTEP]
refine' ⟨And.left, fun hA => ⟨hA, _⟩⟩
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
α : Type v
inst✝² : CommRing α
inst✝¹ : StarRing α
A✝ : Matrix n n α
β : Type v
inst✝ : CommRing β
A : Matrix n n β
hA : star A * A = 1
⊢ A * star A = 1
[PROOFSTEP]
rwa [mul_eq_one_comm] at hA 
