exists_isCartanSubalgebra_engel — Mathlib

English

If K is infinite and L is finite over K, there exists x ∈ L such that engel_K x is a Cartan subalgebra of L.

Русский

Пусть K бесконечно, а L конечномерна над K; тогда существует x ∈ L, для которого engel_K x является картановой подалгеброй L.

LaTeX

$$$[\\text{Infinite } K]\\Rightarrow \\exists x:\\; \\operatorname{engel} K x\\; \\text{IsCartanSubalgebra}(L)$$$

Lean4

theorem exists_isCartanSubalgebra_engel [Infinite K] : ∃ x : L, IsCartanSubalgebra (engel K x) :=
  by
  apply exists_isCartanSubalgebra_engel_of_finrank_le_card
  exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite K›

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