Theorems · Definition · dynamical systems

Polynomial.newtonMap

{R : Type u_1} → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Polynomial R → S → S

Given a single-variable polynomial P with derivative P', this is the map: x ↦ x - P(x) / P'(x). When P'(x) is not a unit we use a junk-value pattern and send x ↦ x.

Defined in

Mathlib.Dynamics.Newton

Cited by

8 results in Mathlib

Foundations

Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra