English
If aeval x P is nilpotent and aeval x (derivative P) is a unit, then for every n, (aeval x P)^{2^n} divides aeval (P.newtonMap^[n] x) P.
Русский
Если aeval x P нильпотентен и aeval x (derivative P) единица, тогда для любого n выполнено делимость: (P(x))^{2^n} делит P(newtonMap^n(x)).
LaTeX
$$$$\bigl( aeval\,x\,P \bigr)^{2^n} \mid aeval\bigl( P.newtonMap^{[n]}(x) \bigr) P.$$$$
Lean4
/-- This is really an auxiliary result, en route to
`Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero`. -/
theorem aeval_pow_two_pow_dvd_aeval_iterate_newtonMap (h : IsNilpotent (aeval x P))
(h' : IsUnit (aeval x <| derivative P)) (n : ℕ) : (aeval x P) ^ (2 ^ n) ∣ aeval (P.newtonMap^[n] x) P := by
induction n with
| zero => simp
| succ n
ih =>
have ⟨d, hd⟩ :=
binomExpansion (P.map (algebraMap R S)) (P.newtonMap^[n] x)
(-Ring.inverse (aeval (P.newtonMap^[n] x) <| derivative P) * aeval (P.newtonMap^[n] x) P)
rw [eval_map_algebraMap, eval_map_algebraMap] at hd
rw [iterate_succ', comp_apply, newtonMap_apply, sub_eq_add_neg, neg_mul_eq_neg_mul, hd]
refine dvd_add ?_ (dvd_mul_of_dvd_right ?_ _)
· convert dvd_zero _
have : IsUnit (aeval (P.newtonMap^[n] x) <| derivative P) :=
isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub h' <| isNilpotent_iterate_newtonMap_sub_of_isNilpotent h n
rw [derivative_map, eval_map_algebraMap, ← mul_assoc, mul_neg, Ring.mul_inverse_cancel _ this, neg_mul, one_mul,
add_neg_cancel]
· rw [neg_mul, even_two.neg_pow, mul_pow, pow_succ, pow_mul]
exact dvd_mul_of_dvd_right (pow_dvd_pow_of_dvd ih 2) _
