isFixedPt_newtonMap_of_isUnit_iff

English

If P'(x) is a unit, then N_P(x) is a fixed point of the Newton map if and only if P(x) = 0.

Русский

Если P'(x) единица, то x фиксирована по карте Ньютона тогда и только тогда, когда P(x) = 0.

LaTeX

$$$$\text{IsFixedPt}(P.newtonMap, x) \iff P(x)=0\quad\text{if } P'(x)\text{ is a unit}.$$$$

Lean4

theorem isFixedPt_newtonMap_of_isUnit_iff (h : IsUnit <| aeval x (derivative P)) :
    IsFixedPt P.newtonMap x ↔ aeval x P = 0 := by
  rw [IsFixedPt, newtonMap_apply, sub_eq_self, Ring.inverse_mul_eq_iff_eq_mul _ _ _ h, mul_zero]

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