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

State before:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ∣ ↑p
Tactic:
show 1 - zeta p ∣ (p : ℤ)
State after:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ∣ ↑↑p

State before:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ∣ ↑↑p
Tactic:
rw [one_sub_zeta_dvd_int_iff]
State after:
no goals