isNilpotent_of_top_iff — Mathlib

English

Equiv between Lie algebras and linear equivalence of modules preserve nilpotency of the module.

Русский

Эквивариант между алгебрами Ли и линейные эквивалентности модулей сохраняют нильпотентность модуля.

LaTeX

$$theorem lieModule_isNilpotent_iff (f,g,hfg) : IsNilpotent L M ↔ IsNilpotent L₂ M₂$$

Lean4

@[simp]
theorem isNilpotent_of_top_iff : IsNilpotent (⊤ : LieSubalgebra R L) M ↔ IsNilpotent L M :=
  Equiv.lieModule_isNilpotent_iff LieSubalgebra.topEquiv (1 : M ≃ₗ[R] M) fun _ _ => rfl

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