comp_eq_sum_left

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

The composition of polynomials equals the sum over monomials: p.comp q = p.sum (e ↦ a ↦ C(a) * q^e).

Русский

Сложение полиномов через композицию даёт p.comp q = p.sum (e ↦ a ↦ C(a) · q^e).

LaTeX

$$$p.\mathrm{comp}\; q = p.\mathrm{sum}\; (\lambda e\ a.\; C\ a \cdot q^e)$$$

Lean4

theorem comp_eq_sum_left : p.comp q = p.sum fun e a => C a * q ^ e := by rw [comp, eval₂_eq_sum]

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

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

Разделы

Аффилиация

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