rank_le_natTrailingDegree_charpoly_ad

English

IsRegular R M x is equivalent to natTrailingDegree of the characteristic polynomial of ad_R L x equaling rank R L.

Русский

IsRegular R M x эквивалентно тому, что natTrailingDegree характеристического многочлена ад_R L x равен rank R L.

LaTeX

$$$$ \\text{IsRegular } R M x \\iff (\\operatorname{toEnd} R L M x).\\operatorname{charpoly}.\\operatorname{natTrailingDegree} = \\operatorname{rank} R L M $$$$

Lean4

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

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