rank_le_card — Mathlib

English

If M is a free R-module with a basis indexed by ιₘ, then the rank of the Lie module L acting on M is bounded above by the number of basis elements; that is rank_R L M ≤ |ιₘ|.

Русский

Пусть R — ненулевое коммутативное кольцо, L — Ли-алгебра над R, и M — свободный модуль над R с базисом, индексируемым ιₘ. Тогда ранг модуля Ли, реализованного на M, не превосходит числа базисных элементов: rank_R L M ≤ |ιₘ|.

LaTeX

$$$$ \\operatorname{rank}_R L M \\le |\\iota_m| $$$$

Lean4

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

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