English
Evaluating a singleton at r yields r^i times the element: eval r (single R i m) = r^i • m.
Русский
Оценивание одиночного элемента даёт r^i умноженное на элемент: eval r (single R i m) = r^i • m.
LaTeX
$$eval r (single R i m) = r^i • m$$
Lean4
/-- Evaluate a polynomial `p : PolynomialModule R M` at `r : R`. -/
@[simps! -isSimp]
noncomputable def eval (r : R) : PolynomialModule R M →ₗ[R] M
where
toFun p := p.sum fun i m => r ^ i • m
map_add' _ _ := Finsupp.sum_add_index' (fun _ => smul_zero _) fun _ _ _ => smul_add _ _ _
map_smul' s
m := by
refine (Finsupp.sum_smul_index' ?_).trans ?_
· exact fun i => smul_zero _
· simp_rw [RingHom.id_apply, Finsupp.smul_sum]
congr
ext i c
rw [smul_comm]
