map_mvPolynomial_eq_eval₂ — Mathlib

English

If every coefficient of a multivariate polynomial p lies in the comap of the C map along an ideal I, then p itself lies in I.

Русский

Если каждый коэффициент многочлена p принадлежит обратному образу под отображением C вдоль идеала I, то сам p принадлежит I.

LaTeX

$$$\\forall m,\\; p_{coeff}(m) \\in I \\ \Rightarrow\ \ p \\in I$$$

Lean4

theorem map_mvPolynomial_eq_eval₂ {S : Type*} [CommSemiring S] [Finite σ] (ϕ : MvPolynomial σ R →+* S)
    (p : MvPolynomial σ R) : ϕ p = MvPolynomial.eval₂ (ϕ.comp MvPolynomial.C) (fun s => ϕ (MvPolynomial.X s)) p :=
  by
  cases nonempty_fintype σ
  refine Trans.trans (congr_arg ϕ (MvPolynomial.as_sum p)) ?_
  rw [MvPolynomial.eval₂_eq', map_sum ϕ]
  congr
  ext
  simp only [monomial_eq, ϕ.map_pow, map_prod ϕ, ϕ.comp_apply, ϕ.map_mul, Finsupp.prod_pow]

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