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