Theorem: CyclotomicIntegers.one_sub_zeta_mem_nonZeroDivisors (FltRegular/NumberTheory/CyclotomicRing.lean)

State before:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ∈ nonZeroDivisors (CyclotomicIntegers p)
Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero]
State after:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ≠ 0

State before:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ≠ 0
Tactic:
exact (prime_one_sub_zeta p).1
State after:
no goals