taylor_mul

Mathlib.Algebra.Polynomial.Taylor

URI: https://scilib.ai/kg/mathlib#Polynomial.taylor_mul

English

Taylor shift preserves products: taylor r (p q) = taylor r p · taylor r q.

Русский

Сдвиг Тейлора по r сохраняет произведение: taylor r (p q) = taylor r p · taylor r q.

LaTeX

$$$$ \\operatorname{taylor}(r, p q) = \\operatorname{taylor}(r,p) \\cdot \\operatorname{taylor}(r,q). $$$$

Lean4

@[simp]
theorem taylor_mul (p q : R[X]) : taylor r (p * q) = taylor r p * taylor r q :=
  mul_comp ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru