rank_le_card

Mathlib.Algebra.Lie.Rank

URI: https://scilib.ai/kg/mathlib#LieAlgebra.rank_le_card

English

For a fixed basis b of L, rank_R L ≤ |ι|.

Русский

Для фиксированного базиса b Ли-алгебры L выполняется неравенство ранга: rank_R L ≤ |ι|.

LaTeX

$$$$ \\operatorname{rank}_R L \\le |\\iota| $$$$

Lean4

theorem rank_le_card [Nontrivial R] : rank R L ≤ Fintype.card ι :=
  nilRank_le_card _ b

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru