case pos
l : Type ?u.242378
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)
⊢ det A⁻¹ = Ring.inverse (det A)

case neg
l : Type ?u.242378
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)
⊢ det A⁻¹ = Ring.inverse (det A)
l : Type ?u.242378
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ det A⁻¹ = Ring.inverse (det A)
by_cases h : IsUnit A.det
case neg.inl
l : Type ?u.242378
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)
h✝ : IsEmpty n
⊢ det A⁻¹ = Ring.inverse (det A)

case neg.inr
l : Type ?u.242378
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)
h✝ : Nonempty n
⊢ det A⁻¹ = Ring.inverse (det A)
case neg
l : Type ?u.242378
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)
⊢ det A⁻¹ = Ring.inverse (det A)
cases isEmpty_or_nonempty n
case pos.intro
l : Type ?u.242378
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 (det A)
⊢ det A⁻¹ = Ring.inverse (det A)
case pos
l : Type ?u.242378
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)
⊢ det A⁻¹ = Ring.inverse (det A)
cases h.nonempty_invertible
case pos.intro
l : Type ?u.242378
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 (det A)
this : Invertible A := invertibleOfDetInvertible A
⊢ det A⁻¹ = Ring.inverse (det A)
case pos.intro
l : Type ?u.242378
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 (det A)
⊢ det A⁻¹ = Ring.inverse (det A)
letI := invertibleOfDetInvertible A
no goals
case pos.intro
l : Type ?u.242378
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 (det A)
this : Invertible A := invertibleOfDetInvertible A
⊢ det A⁻¹ = Ring.inverse (det A)
rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]
no goals
case neg.inl
l : Type ?u.242378
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)
h✝ : IsEmpty n
⊢ det A⁻¹ = Ring.inverse (det A)
rw [det_isEmpty, det_isEmpty, Ring.inverse_one]
no goals
case neg.inr
l : Type ?u.242378
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)
h✝ : Nonempty n
⊢ det A⁻¹ = Ring.inverse (det A)
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]