English
The regularity of x, in the Lie module sense, is equivalent to the nonvanishing of the rank-th coefficient of the characteristic polynomial of the endomorphism ad_R L x.
Русский
Регулярность элемента x в Ли-модуле эквивалентна ненулевости коэффициента ранга в характеристическом многочлене эндоморфизма ad_R L x.
LaTeX
$$$$ \\text{IsRegular } R M x \\iff (toEnd R L M x).\\operatorname{charpoly}.\\operatorname{coeff}(\\operatorname{rank} R L M) \\neq 0 $$$$
Lean4
/-- Let `x` be an element of a Lie algebra `L` over `R`, and write `n` for `rank R L`.
Then `x` is *regular*
if the `n`-th coefficient of the characteristic polynomial of `ad R L x` is non-zero. -/
def IsRegular (x : L) : Prop :=
LinearMap.IsNilRegular φ x
