English
Let p be a multivariate polynomial over a commutative semiring R, let s be a scalar in R, and let x be a point assigning to each variable a value in R. Then evaluating the scalar multiple s·p at x yields s times the evaluation of p at x: eval_x(s·p) = s·eval_x(p).
Русский
Пусть p — многочлен в нескольких переменных над коммутативным полукольцом R, пусть s ∈ R, и пусть x — задание значений переменным. Тогда вычисление скалярного умножения на p даёт: eval_x(s·p) = s·eval_x(p).
LaTeX
$$$$\operatorname{eval}_x\bigl( s \cdot p \bigr) = s \cdot \operatorname{eval}_x(p).$$$$
Lean4
@[simp]
theorem smul_eval (x) (p : MvPolynomial σ R) (s) : eval x (s • p) = s * eval x p := by
rw [smul_eq_C_mul, (eval x).map_mul, eval_C]
