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 α
this : A ⬝ (adjugate A ⬝ adjugate (adjugate A)) = A ⬝ (det A ^ (Fintype.card n - 1) • 1)
⊢ det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A
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 α
⊢ det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A
have : A ⬝ (A.adjugate ⬝ A.adjugate.adjugate) =
    A ⬝ (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by
  rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
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 α
this : A ⬝ (adjugate A ⬝ adjugate (adjugate A)) = A ⬝ (det A ^ (Fintype.card n - 1) • 1)
⊢ det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A
rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
  Matrix.one_mul] at this
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 ⬝ adjugate (adjugate A)) = A ⬝ (det A ^ (Fintype.card n - 1) • 1)
rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]