English
Let p ∈ R[X], q ∈ PolynomialModule R M, and r ∈ R. Then the evaluation at r of the composition of p with q equals the evaluation at p(r) of q; i.e., eval r (comp p q) = eval (p.eval r) q.
Русский
Пусть p ∈ R[X], q ∈ PolynomialModule R M и r ∈ R. Тогда вычисление по значению r композиции p и q равняется вычислению по значению p(r) для q; то есть eval r (comp p q) = eval (p.eval r) q.
LaTeX
$$$\operatorname{eval}_r(\operatorname{comp}(p,q)) = \operatorname{eval}(p.\operatorname{eval}(r))(q).$$$
Lean4
theorem comp_eval (p : R[X]) (q : PolynomialModule R M) (r : R) : eval r (comp p q) = eval (p.eval r) q :=
by
rw [← LinearMap.comp_apply]
induction q using induction_linear with
| zero => simp_rw [map_zero]
| add _ _ e₁ e₂ => simp_rw [map_add, e₁, e₂]
| single i m =>
rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]
module
