n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : IsUnit (det (A ^ z))
⊢ A ^ z ≠ 0
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
⊢ A ^ z ≠ 0
have := ha.det_zpow z
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
⊢ IsUnit (det (A ^ z)) → A ^ z ≠ 0
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : IsUnit (det (A ^ z))
⊢ A ^ z ≠ 0
revert this
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
⊢ ¬A ^ z ≠ 0 → ¬IsUnit (det (A ^ z))
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
⊢ IsUnit (det (A ^ z)) → A ^ z ≠ 0
contrapose!
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
⊢ A ^ z = 0 → ¬IsUnit (det (A ^ z))
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
⊢ ¬A ^ z ≠ 0 → ¬IsUnit (det (A ^ z))
rw [ne_eq, not_not]
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit (det (A ^ z))
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
⊢ A ^ z = 0 → ¬IsUnit (det (A ^ z))
intro this
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit 0
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit (det (A ^ z))
rw [this, det_zero ‹_›]
no goals
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit 0
exact not_isUnit_zero