case hz
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ IsUnit (det (A ^ 0)) ↔ IsUnit (det A) ∨ 0 = 0

case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ ↑z)) ↔ IsUnit (det A) ∨ ↑z = 0
⊢ IsUnit (det (A ^ (↑z + 1))) ↔ IsUnit (det A) ∨ ↑z + 1 = 0

case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ (-↑z))) ↔ IsUnit (det A) ∨ -↑z = 0
⊢ IsUnit (det (A ^ (-↑z - 1))) ↔ IsUnit (det A) ∨ -↑z - 1 = 0
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℤ
⊢ IsUnit (det (A ^ z)) ↔ IsUnit (det A) ∨ z = 0
induction' z using Int.induction_on with z _ z _
no goals
case hz
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ IsUnit (det (A ^ 0)) ↔ IsUnit (det A) ∨ 0 = 0
simp
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ ↑z)) ↔ IsUnit (det A) ∨ ↑z = 0
⊢ IsUnit (det A) ↔ IsUnit (det A) ∨ Nat.succ z = 0
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ ↑z)) ↔ IsUnit (det A) ∨ ↑z = 0
⊢ IsUnit (det (A ^ (↑z + 1))) ↔ IsUnit (det A) ∨ ↑z + 1 = 0
rw [← Int.ofNat_succ, zpow_ofNat, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero, Int.ofNat_inj]
no goals
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ ↑z)) ↔ IsUnit (det A) ∨ ↑z = 0
⊢ IsUnit (det A) ↔ IsUnit (det A) ∨ Nat.succ z = 0
simp
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ (-↑z))) ↔ IsUnit (det A) ∨ -↑z = 0
⊢ IsUnit (det A) ↔ IsUnit (det A) ∨ Nat.succ z = 0
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ (-↑z))) ↔ IsUnit (det A) ∨ -↑z = 0
⊢ IsUnit (det (A ^ (-↑z - 1))) ↔ IsUnit (det A) ∨ -↑z - 1 = 0
rw [← neg_add', ← Int.ofNat_succ, zpow_neg_coe_nat, isUnit_nonsing_inv_det_iff, det_pow,
  isUnit_pow_succ_iff, neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]
no goals
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ (-↑z))) ↔ IsUnit (det A) ∨ -↑z = 0
⊢ IsUnit (det A) ↔ IsUnit (det A) ∨ Nat.succ z = 0
simp