comp_smul — Mathlib

English

Let p, p' be polynomials in R[X] and q ∈ PolynomialModule R M. Then composition with p distributes over scalar multiplication: comp(p, p' · q) = (p' · p) ∘ p · comp(p, q); i.e., comp p (p' • q) = p'.comp p · comp p q.

Русский

Пусть p, p' — многочлены из R[X], q ∈ PolynomialModule R M. Тогда композиция с p распределяет над скалярами: comp(p, p' · q) = (p' ∘ p) · comp(p, q).

LaTeX

$$$\operatorname{comp}(p, (p'\,\cdot\, q)) = (p'.\operatorname{comp}(p)) \cdot \operatorname{comp}(p,q).$$$

Lean4

theorem comp_smul (p p' : R[X]) (q : PolynomialModule R M) : comp p (p' • q) = p'.comp p • comp p q :=
  by
  rw [comp_apply, map_smul, eval_smul, Polynomial.comp, Polynomial.eval_map, comp_apply]
  rfl

Похожие утверждения