l : Type ?u.302074
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : IsUnit (det A)
⊢ ((IsUnit.unit h)⁻¹ • A) ⬝ adjugate A = 1
l : Type ?u.302074
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : IsUnit (det A)
⊢ (adjugate A)⁻¹ = (IsUnit.unit h)⁻¹ • A
refine' inv_eq_left_inv _
no goals
l : Type ?u.302074
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : IsUnit (det A)
⊢ ((IsUnit.unit h)⁻¹ • A) ⬝ adjugate A = 1
rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]