English
Let R be a commutative semiring and σ a type. For every natural number n with n ≥ 2, the constant polynomial corresponding to n in the multivariate polynomial ring MvPolynomial(σ, R) evaluates to the same natural number n under any RingHom f: R →+* S and any function g: σ → S; that is, (ofNat(n) : MvPolynomial(σ, R)).eval₂ f g = ofNat(n).
Русский
Пусть R — коммутативная полугруппа с единицей, σ — множество. Для каждого натурального числа n, удовлетворяющего условию n ≥ 2, константный многочлен соответствующий n в кольце MvPolynomial(σ, R) при любом гомоморфизме колец f: R →+* S и любом отображении g: σ → S принимает то же число n; то есть (ofNat(n) : MvPolynomial(σ, R)).eval₂ f g = ofNat(n).
LaTeX
$$$ (\operatorname{ofNat}(n) : \mathrm{MvPolynomial}(\sigma, R)).\operatorname{eval}_2 f g = \operatorname{ofNat}(n) $$$
Lean4
@[simp]
theorem eval₂_ofNat (n : Nat) [n.AtLeastTwo] : (ofNat(n) : MvPolynomial σ R).eval₂ f g = ofNat(n) :=
eval₂_natCast f g n
