isNilpotent_aeval_sub_of_isNilpotent_sub

English

If a − b is nilpotent in the algebra, then aeval a P − aeval b P is nilpotent for any P ∈ R[X].

Русский

Если a − b нильпотентно в алгебре, то для любого полинома P ∈ R[X] выражение aeval a P − aeval b P нильпотентно.

LaTeX

$$$\operatorname{IsNilpotent}(a - b) \Rightarrow \operatorname{IsNilpotent}(\operatorname{aeval}(a, P) - \operatorname{aeval}(b, P))$$$

Lean4

theorem isNilpotent_aeval_sub_of_isNilpotent_sub (h : IsNilpotent (a - b)) : IsNilpotent (aeval a P - aeval b P) :=
  by
  simp only [← eval_map_algebraMap]
  have ⟨c, hc⟩ := evalSubFactor (map (algebraMap R S) P) a b
  exact hc ▸ (Commute.all _ _).isNilpotent_mul_left h

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