English
The evaluation map is linear with respect to the polynomial action: eval r (p • q) = p.eval r • eval r q.
Русский
Оценка на r линейна по действию по полиному: eval r (p • q) = (p.eval r) • eval r q.
LaTeX
$$$\\operatorname{eval} r (p \\cdot q) = (p.\\operatorname{eval} r) \\cdot (\\operatorname{eval} r q)$$$
Lean4
@[simp]
theorem eval_smul (p : R[X]) (q : PolynomialModule R M) (r : R) : eval r (p • q) = p.eval r • eval r q := by
induction q using induction_linear with
| zero => rw [smul_zero, map_zero, smul_zero]
| add f g e₁ e₂ => rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
| single i m =>
induction p using Polynomial.induction_on' with
| add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
| monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module
