classical
have key : _ = (p : 𝓞 K) := @Polynomial.eval_one_cyclotomic_prime _ _ _ hp
rw [cyclotomic_eq_prod_X_sub_primitiveRoots hζ.unit'_coe, eval_prod] at key
simp only [eval_sub, eval_X, eval_C] at key
have : {↑hζ.unit'} ⊆ primitiveRoots p (𝓞 K) := by simpa using hζ.unit'_coe
rw [← Finset.prod_sdiff this, Finset.prod_singleton] at key
rw [← key]
have := (Ideal.neg_mem_iff I).mpr (Ideal.subset_span (Set.mem_singleton ζ1))
rw [neg_sub] at this
exact Ideal.mul_mem_left _ _ this
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
no goals