isNilpotent_range_toEnd_iff — Mathlib

English

Nilpotence of the range of toEnd coincides with nilpotence of the Lie algebra action on M.

Русский

Нильпотентность диапазона отображения toEnd совпадает с нильпотентностью действия Ли-алгебры на M.

LaTeX

$$$\\operatorname{IsNilpotent}((\\operatorname{toEnd} R L M).\\mathrm{range}\,M) \\iff \\operatorname{IsNilpotent}_L(M).$$$

Lean4

@[simp]
theorem isNilpotent_range_toEnd_iff : IsNilpotent (toEnd R L M).range M ↔ IsNilpotent L M :=
  by
  simp only [isNilpotent_iff R _ M]
  constructor <;> rintro ⟨k, hk⟩ <;> use k <;> rw [← LieSubmodule.toSubmodule_inj] at hk ⊢ <;> simpa using hk

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