eval_mem — Mathlib

English

If a polynomial p over S has all its coefficients in a subsemiring s, and all inputs v lie in s, then eval v p lies in s.

Русский

Если коэффициенты p лежат в подполе s и аргументы v лежат в s, то eval v p ∈ s.

LaTeX

$$$$ \forall p \in MvPolynomial(σ,S), \forall s, (\forall i \in p.support, p(coeff i) \in s) \Rightarrow (\forall v, v(i) \in s) \Rightarrow MvPolynomial.eval v p \in s. $$$$

Lean4

theorem eval_mem {p : MvPolynomial σ S} {s : subS} (hs : ∀ i ∈ p.support, p.coeff i ∈ s) {v : σ → S}
    (hv : ∀ i, v i ∈ s) : MvPolynomial.eval v p ∈ s :=
  eval₂_mem hs hv

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