English
Let R, S, A be commutative semirings with S-algebra structures as in the setting. For any algebra hom g: R →ₐ[S] A and any linear map y: σ → A, and for every natural number n with n ≥ 2, the evaluation tower sends the constant polynomial ofNat(n) to itself:
Русский
Пусть R, S, A — коммутативные полускольца и имеется структура S-алгебры, далее задан г: R →ₐ[S] A и y: σ → A. Тогда для любого n ≥ 2 константный полином ofNat(n) удовлетворяет: aevalTower(g,y)(ofNat(n)) = ofNat(n).
LaTeX
$$$\operatorname{aevalTower}(g,y)(\operatorname{ofNat}(n)) = \operatorname{ofNat}(n).$$$
Lean4
@[simp]
theorem aevalTower_ofNat (n : Nat) [n.AtLeastTwo] : aevalTower g y (ofNat(n) : MvPolynomial σ R) = ofNat(n) :=
_root_.map_ofNat _ _
