English
For any ring hom g, polynomial p, element x in the target, and s in the source, eval₂ g x (s • p) = g(s) · eval₂ g x p.
Русский
Для любого кольцевого гомоморфа g, полинома p, элемента x и скаляра s: eval₂ g x (s • p) = g(s) · eval₂ g x p.
LaTeX
$$$\\operatorname{eval}_2 g x (s \\cdot p) = g(s) \\cdot \\operatorname{eval}_2 g x p$$$
Lean4
@[simp]
theorem eval₂_smul (g : R →+* S) (p : R[X]) (x : S) {s : R} : eval₂ g x (s • p) = g s * eval₂ g x p :=
by
have A : p.natDegree < p.natDegree.succ := Nat.lt_succ_self _
have B : (s • p).natDegree < p.natDegree.succ := (natDegree_smul_le _ _).trans_lt A
rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B] <;> simp [mul_sum, mul_assoc]
