no goals
l : Type ?u.248103
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⁻¹⁻¹ = 1 ⬝ A⁻¹⁻¹
rw [Matrix.one_mul]
no goals
l : Type ?u.248103
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)
⊢ 1 ⬝ A⁻¹⁻¹ = A ⬝ A⁻¹ ⬝ A⁻¹⁻¹
rw [A.mul_nonsing_inv h]
no goals
l : Type ?u.248103
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⁻¹ ⬝ A⁻¹⁻¹ = A
rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_one]