rank_le_natTrailingDegree_charpoly_ad

English

For any x in L, the rank of the Lie module L on M is bounded above by the natTrailingDegree of the characteristic polynomial of ad_R L x: rank_R L M ≤ (toEnd R L M x).charpoly.natTrailingDegree.

Русский

Пусть x ∈ L. Тогда ранг модуля Ли на M не превосходит natTrailingDegree характеристического многочлена ад(x): rank_R L M ≤ (toEnd R L M x).charpoly.natTrailingDegree.

LaTeX

$$$$ \\operatorname{rank}_R L M \\le (\\operatorname{toEnd} R L M\\, x).\\operatorname{charpoly}.\\operatorname{natTrailingDegree} $$$$

Lean4

theorem rank_le_natTrailingDegree_charpoly_ad [Nontrivial R] :
    rank R L M ≤ (toEnd R L M x).charpoly.natTrailingDegree :=
  nilRank_le_natTrailingDegree_charpoly _ _

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