rw [natDegree_cyclotomic] at this
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
this : (cyclotomic p ℤ).natDegree = 0
⊢ False
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
this : p.totient = 0
⊢ False