polynomial_mem_ideal_of_coeff_mem_ideal

English

If every coefficient of a polynomial p lies in an ideal I (via the coefficient map from R to R[X]), then p itself lies in I.

Русский

Если каждая коэффициентная составляющая полинома p принадлежит идеалу I (через отображение коэффициентов), то и сам полином p принадлежит I.

LaTeX

$$$\\forall p \\in R[X],\\ (\\forall n, \\operatorname{coeff}(p,n) \\in I) \\implies p \\in I$, more precisely: If $hp: \\forall n, p_{n} \\in I$ (via comap of $C$), then $p \\in I$.$$

Lean4

/-- If every coefficient of a polynomial is in an ideal `I`, then so is the polynomial itself -/
theorem polynomial_mem_ideal_of_coeff_mem_ideal (I : Ideal R[X]) (p : R[X])
    (hp : ∀ n : ℕ, p.coeff n ∈ I.comap (C : R →+* R[X])) : p ∈ I :=
  sum_C_mul_X_pow_eq p ▸ Submodule.sum_mem I fun n _ => I.mul_mem_right _ (hp n)

Похожие утверждения