case pos
l : Type ?u.348186
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)
⊢ A⁻¹⁻¹⁻¹ = A⁻¹

case neg
l : Type ?u.348186
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)
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
l : Type ?u.348186
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
by_cases h : IsUnit A.det
no goals
case pos
l : Type ?u.348186
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)
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
rw [nonsing_inv_nonsing_inv _ h]
no goals
case neg
l : Type ?u.348186
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)
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
simp [nonsing_inv_apply_not_isUnit _ h]