isNilpotent_iterate_newtonMap_sub_of_isNilpotent

English

If aeval x P is nilpotent, then for every n, the difference P.newtonMap^[n] x − x is nilpotent.

Русский

Если P(x) = aeval x P никоим образом нильпотентен, то для каждого n разность P.newtonMap^[n] x − x нильпотентна.

LaTeX

$$$$\text{IsNilpotent}(P.newtonMap^{[n]}(x) - x)\quad\text{for all } n \in \mathbb{N}.$$$$

Lean4

theorem isNilpotent_iterate_newtonMap_sub_of_isNilpotent (h : IsNilpotent <| aeval x P) (n : ℕ) :
    IsNilpotent <| P.newtonMap^[n] x - x := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [iterate_succ', comp_apply, newtonMap_apply, sub_right_comm]
    refine (Commute.all _ _).isNilpotent_sub ih <| (Commute.all _ _).isNilpotent_mul_left ?_
    simpa using Commute.isNilpotent_add (Commute.all _ _) (isNilpotent_aeval_sub_of_isNilpotent_sub P ih) h

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