l : Type ?u.349525
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
⊢ Ring.inverse (det (A ⬝ B)) • adjugate (A ⬝ B) =
    (Ring.inverse (det B) • adjugate B) ⬝ (Ring.inverse (det A) • adjugate A)
l : Type ?u.349525
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
⊢ (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹
simp only [inv_def]
no goals
l : Type ?u.349525
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
⊢ Ring.inverse (det (A ⬝ B)) • adjugate (A ⬝ B) =
    (Ring.inverse (det B) • adjugate B) ⬝ (Ring.inverse (det A) • adjugate A)
rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
  Ring.mul_inverse_rev]