Polynomial.newtonMap_apply

theorem Polynomial.newtonMap_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Polynomial R) {x : S}, P.newtonMap x = x - Ring.inverse ((Polynomial.aeval x) (Polynomial.derivative P)) * (Polynomial.aeval x) P

This theorem states that for any commutative ring `R`, any other commutative ring `S`, any `R`-algebra structure on `S`, and any polynomial `P` over `R`, the value of the Newton map of `P` at any point `x` in `S` is equal to `x` minus the product of the inverse of the evaluation of the derivative of `P` at `x` and the evaluation of `P` at `x`. If the derivative of `P` evaluated at `x` is not a unit (i.e., it cannot be inverted), then the Ring.inverse function returns zero for this term.

More concisely: For any commutative rings `R` and `S`, `R-algebra` `S`, polynomial `P` over `R`, and `x` in `S`, the Newton map of `P` at `x` equals `x - P'(x)⁻¹ * P(x)`, where `P'(x)` is the derivative of `P` at `x` and `⁻¹` denotes the multiplicative inverse. If `P'(x)` is not a unit, then `P'(x)⁻¹` is zero.