exists_isRegular_of_finrank_le_card

English

For a Lie algebra L over a domain R, if finrank_R L ≤ #R, there exists x ∈ L that is regular.

Русский

Для Ли-алгебры L над доменом R, если финальный ранг ограничен #R, существует x ∈ L, который регулярен.

LaTeX

$$$$ \\exists x : L, \\; \\text{IsRegular } R x $$$$

Lean4

theorem exists_isRegular_of_finrank_le_card (h : finrank R L ≤ #R) : ∃ x : L, IsRegular R x :=
  LinearMap.exists_isNilRegular_of_finrank_le_card _ h

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