exact zeta_sub_one_dvd_Int_iff H
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ ⋯.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n
no goals