span_le_of_C_coeff_mem — Mathlib

English

If a polynomial’s coefficients lie in an ideal I, then the span of the polynomials C(coeff f i) lies in I.

Русский

Если коэффициенты полинома принадлежат идеалу I, то порождающее множество C(coeff f i) лежит в I.

LaTeX

$$Ideal.span { g | ∃ i, g = C (f.coeff i) } ≤ I$$

Lean4

/-- If the coefficients of a polynomial belong to an ideal, then that ideal contains
the ideal spanned by the coefficients of the polynomial. -/
theorem span_le_of_C_coeff_mem (cf : ∀ i : ℕ, C (f.coeff i) ∈ I) : Ideal.span {g | ∃ i, g = C (f.coeff i)} ≤ I :=
  by
  simp only [@eq_comm _ _ (C _)]
  exact (Ideal.span_le.trans range_subset_iff).mpr cf

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