English
An element f of the polynomial ring lies in the ideal map of I iff every coefficient of f lies in I.
Русский
Элемент f многочленового кольца принадлежит образу идеала I, если и только если каждый коэффициент f принадлежит I.
LaTeX
$$$f \in \operatorname{Ideal.map}(\mathrm{C} : R \to R[σ])\ I \;\iff\; \forall m, \; \mathrm{coeff}(m,f) \in I$$$
Lean4
/-- If every coefficient of a polynomial is in an ideal `I`, then so is the polynomial itself,
multivariate version. -/
theorem mem_ideal_of_coeff_mem_ideal (I : Ideal (MvPolynomial σ R)) (p : MvPolynomial σ R)
(hcoe : ∀ m : σ →₀ ℕ, p.coeff m ∈ I.comap (C : R →+* MvPolynomial σ R)) : p ∈ I :=
by
rw [as_sum p]
suffices ∀ m ∈ p.support, monomial m (MvPolynomial.coeff m p) ∈ I by exact Submodule.sum_mem I this
intro m _
rw [← mul_one (coeff m p), ← C_mul_monomial]
suffices C (coeff m p) ∈ I by exact I.mul_mem_right (monomial m 1) this
simpa [Ideal.mem_comap] using hcoe m
