isNilpotent_toEnd_of_isNilpotent₂

English

For x,y in L, the endomorphism toEnd x composed with toEnd y is nilpotent.

Русский

Для x,y ∈ L, композиция toEnd(x) ∘ toEnd(y) нильпотентна.

LaTeX

$$IsNilpotent (toEnd R L M x ∘ₗ toEnd R L M y)$$

Lean4

theorem isNilpotent_toEnd_of_isNilpotent₂ [IsNilpotent L M] (x y : L) :
    _root_.IsNilpotent (toEnd R L M x ∘ₗ toEnd R L M y) :=
  by
  obtain ⟨k, hM⟩ := IsNilpotent.nilpotent R L M
  replace hM : lowerCentralSeries R L M (2 * k) = ⊥ := by rw [eq_bot_iff, ← hM];
    exact antitone_lowerCentralSeries R L M (by cutsat)
  use k
  ext m
  rw [Module.End.pow_apply, LinearMap.zero_apply, ← LieSubmodule.mem_bot (R := R) (L := L), ← hM]
  exact iterate_toEnd_mem_lowerCentralSeries₂ R L M x y m k

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