X_mul_divX_add

Mathlib.Algebra.Polynomial.Inductions

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

English

The identity X * divX p + C(p.coeff 0) = p holds for all p ∈ R[X].

Русский

Идентичность X * divX p + C(p.coeff 0) = p верна для всех p ∈ R[X].

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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