taylor_taylor — Mathlib

English

Taylor shifts add under composition: taylor r (taylor s f) = taylor (r + s) f.

Русский

Сдвиги Тейлора складываются при композиции: taylor r (taylor s f) = taylor (r + s) f.

LaTeX

$$$$ \\operatorname{taylor}(r, \\operatorname{taylor}(s,f)) = \\operatorname{taylor}(r+s, f). $$$$

Lean4

theorem taylor_taylor (f : R[X]) (r s : R) : taylor r (taylor s f) = taylor (r + s) f := by
  simp only [taylor_apply, comp_assoc, map_add, add_comp, X_comp, C_comp, add_assoc]

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