English
If a polynomial p over R has all its coefficients mapped into a subsemiring s under a RingHom f, and all inputs v lie in s, then eval₂ f v p lies in s.
Русский
Если коэффициенты полинома p отображаются в подполе s через гомоморфизм f и все аргументы v лежат в s, тогда eval₂ f v p ∈ s.
LaTeX
$$$$ \forall f, p, s, (\forall i \in p.support, f(p.coeff(i)) \in s) \Rightarrow (\forall v, v(i) \in s) \Rightarrow MvPolynomial.eval₂ f v p \in s. $$$$
Lean4
theorem eval₂_mem {f : R →+* S} {p : MvPolynomial σ R} {s : subS} (hs : ∀ i ∈ p.support, f (p.coeff i) ∈ s) {v : σ → S}
(hv : ∀ i, v i ∈ s) : MvPolynomial.eval₂ f v p ∈ s := by
classical
replace hs : ∀ i, f (p.coeff i) ∈ s := by
intro i
by_cases hi : i ∈ p.support
· exact hs i hi
· rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]
exact zero_mem s
induction p using MvPolynomial.monomial_add_induction_on with
| C a => simpa using hs 0
| monomial_add a b f ha _ ih =>
rw [eval₂_add, eval₂_monomial]
refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
· simpa [MvPolynomial.notMem_support_iff.1 ha] using hs a
have := hs i
rw [coeff_add, coeff_monomial] at this
split_ifs at this with h
· subst h
rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]
exact zero_mem _
· rwa [zero_add] at this
