simp only [eval_sub, eval_X, eval_C] at key
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ j ∈ primitiveRoots (↑p) (𝓞 K), eval 1 (X - C j) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}