English
Let R be a commutative ring and M an R-module. For any polynomial p ∈ R[X], any natural i, and any m ∈ M, the composition of p with the polynomial that represents m at degree i equals p^i acting on the constant polynomial m; i.e., comp(p, single(R, i, m)) = p^i · single(R, 0, m).
Русский
Пусть R—коммутативное кольцо, M — R-модуль. Для любого многочлена p ∈ R[X], любого натурального i и любого элемента m ∈ M композиция p с полиномом, представляющим m в степени i, равна p^i, умноженному на константный полином m; то есть comp(p, single(R, i, m)) = p^i · single(R, 0, m).
LaTeX
$$$\operatorname{comp}(p,\ \operatorname{single}(R,i,m)) = p^{\,i} \cdot \operatorname{single}(R,0,m).$$$
Lean4
theorem comp_single (p : R[X]) (i : ℕ) (m : M) : comp p (single R i m) = p ^ i • single R 0 m :=
by
rw [comp_apply, map_single, eval_single]
rfl
