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)
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)
simp only [coe_toGL, toLin'_mul]
no goals
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)
rfl