no goals
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ adjugate A ⬝ A = (Aᵀ ⬝ adjugate Aᵀ)ᵀ
rw [← adjugate_transpose, ← transpose_mul, transpose_transpose]
no goals
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ (Aᵀ ⬝ adjugate Aᵀ)ᵀ = det A • 1
rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]