English
Let R be a semiring and S a semiring with R-module structure, with IsScalarTower R S S. For any p ∈ R[X] and x ∈ S, the two ways of evaluating p at x agree: p.eval₂ RingHom.smulOneHom x = p.smeval x.
Русский
Пусть R — полукольцо и S — полукольцо с модулем над R и т. д. При любых p ∈ R[X] и x ∈ S оба способа вычисления p в x совпадают: p.eval₂ RingHom.smulOneHom x = p.smeval x.
LaTeX
$$$$ \forall (R : Type*) [\mathrm{Semiring}~R] \{S : Type*\} [\mathrm{Semiring}~S] [\mathrm{Module}~R~S] [\mathrm{IsScalarTower}~R~S~S] (p : R[X]) (x : S), p.eval₂ RingHom.smulOneHom x = p.smeval x. $$$$
Lean4
theorem eval₂_smulOneHom_eq_smeval (R : Type*) [Semiring R] {S : Type*} [Semiring S] [Module R S] [IsScalarTower R S S]
(p : R[X]) (x : S) : p.eval₂ RingHom.smulOneHom x = p.smeval x :=
by
rw [smeval_eq_sum, eval₂_eq_sum]
congr 1 with e a
simp only [RingHom.smulOneHom_apply, smul_one_mul, smul_pow]
