divX_hom_toFun

Mathlib.Algebra.Polynomial.Inductions

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

English

The underlying function of the additive endomorphism divX_hom is exactly the function divX.

Русский

Функция, лежащая в основе делителя divX_hom, равна функции divX.

LaTeX

$$$\\text{divX\_hom}\\; p = \\operatorname{divX}(p)$ for all polynomials p.$$

Lean4

@[simp]
theorem divX_hom_toFun : divX_hom p = divX p :=
  rfl

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

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

Разделы

Аффилиация

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