Theorems · Theorem · dynamical systems

Polynomial.aeval_pow_two_pow_dvd_aeval_iterate_newtonMap

∀ {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},
  IsNilpotent ((Polynomial.aeval x) P) →
    IsUnit ((Polynomial.aeval x) (Polynomial.derivative P)) →
      ∀ (n : ℕ), (Polynomial.aeval x) P ^ 2 ^ n ∣ (Polynomial.aeval (P.newtonMap^[n] x)) P

This is really an auxiliary result, en route to Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero.

Defined in

Mathlib.Dynamics.Newton

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra