English
If f ∉ I, then there exists i with C(coeff f i) ∉ I.
Русский
Если f не принадлежит I, то существует индекс i, для которого C(coeff f i) не принадлежит I.
LaTeX
$$f ∉ I → ∃ i, C (f.coeff i) ∉ I$$
Lean4
theorem mem_span_C_coeff : f ∈ Ideal.span {g : R[X] | ∃ i : ℕ, g = C (coeff f i)} :=
by
let p := Ideal.span {g : R[X] | ∃ i : ℕ, g = C (coeff f i)}
nth_rw 2 [(sum_C_mul_X_pow_eq f).symm]
refine Submodule.sum_mem _ fun n _hn => ?_
dsimp
have : C (coeff f n) ∈ p := by
apply subset_span
rw [mem_setOf_eq]
use n
have : monomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this
convert this using 1
simp only [monomial_mul_C, one_mul, smul_eq_mul]
rw [← C_mul_X_pow_eq_monomial]
