newtonMap_apply_of_not_isUnit

Mathlib.Dynamics.Newton

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

English

If P'(x) is not a unit, then the Newton map fixes x: N_P(x) = x.

Русский

Если P'(x) не единица, то N_P(x) = x.

LaTeX

$$$$P.newtonMap(x) = x.$$$$

Lean4

theorem newtonMap_apply_of_not_isUnit (h : ¬(IsUnit <| aeval x (derivative P))) : P.newtonMap x = x := by
  simp [newtonMap_apply, Ring.inverse, h]

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

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

Разделы

Аффилиация

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