case intro
l : Type ?u.190911
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible A
⊢ A ⬝ A⁻¹ = 1
l : Type ?u.190911
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A ⬝ A⁻¹ = 1
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
no goals
case intro
l : Type ?u.190911
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible A
⊢ A ⬝ A⁻¹ = 1
rw [← invOf_eq_nonsing_inv, Matrix.mul_invOf_self]