divX_mul_X_add

Mathlib.Algebra.Polynomial.Inductions

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

English

For any p ∈ R[X], X · divX p + C(p.coeff 0) = p.

Русский

Для любого p ∈ R[X], X·divX p + C(p.coeff 0) = p.

LaTeX

$$$X \\cdot \\operatorname{divX}(p) + C(p_0) = p.$$$

Lean4

theorem divX_mul_X_add (p : R[X]) : divX p * X + C (p.coeff 0) = p :=
  ext <| by rintro ⟨_ | _⟩ <;> simp [coeff_C, coeff_mul_X]

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

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

Разделы

Аффилиация

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