finrank_engel — Mathlib

English

The rank of L equals the natTrailingDegree of the characteristic polynomial of ad_R L.

Русский

Ранг Ли-алгебры L равен natTrailingDegree характеристического многочлена ад_R L.

LaTeX

$$$$ \\operatorname{rank}_R L = (\\operatorname{polyCharpoly} (\\operatorname{ad} R L).toLinearMap b).\\operatorname{natTrailingDegree} $$$$

Lean4

theorem finrank_engel (x : L) : finrank K (engel K x) = (ad K L x).charpoly.natTrailingDegree :=
  (ad K L x).finrank_maxGenEigenspace_zero_eq

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