rank_le_finrank_engel — Mathlib

English

For a Lie algebra L over a field K, rank_K L ≤ finrank_K (engel_K x) for any x ∈ L, hence rank ≤ finrank engel of x.

Русский

Для алгебры Ли L над полем K верно: ранг ≤ финразряд Engel(x) для любого x ∈ L.

LaTeX

$$$$ \\operatorname{rank}_K L \\le \\operatorname{finrank}_K (\\operatorname{engel}_K x) $$$$

Lean4

theorem rank_le_finrank_engel (x : L) : rank K L ≤ finrank K (engel K x) :=
  (rank_le_natTrailingDegree_charpoly_ad K x).trans (finrank_engel K x).ge

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