newtonMap_apply_of_isUnit

Mathlib.Dynamics.Newton

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

← MathLib Explorer

English

If P'(x) is a unit (invertible), then N_P(x) = x − P'(x)^{-1} P(x).

Русский

Если P'(x) обратимо, то N_P(x) = x − P'(x)^{-1} P(x).

LaTeX

$$$$P.newtonMap(x) = x - P'(x)^{-1} P(x)\,,$$ когда $P'(x)$ является единицей (обратимым).$$

Lean4

theorem newtonMap_apply_of_isUnit (h : IsUnit <| aeval x (derivative P)) : P.newtonMap x = x - h.unit⁻¹ * aeval x P :=
  by simp [newtonMap_apply, Ring.inverse, h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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