English
Regularity is equivalent to the nonzero of the coefficient at rank in the polyCharpoly of ad_R L.
Русский
Регулярность эквивалентна ненулевому коэффициенту при ранге в polyCharpoly ад_R L.
LaTeX
$$$$ \\text{IsRegular } R x \\iff (\\operatorname{charpoly} (\\operatorname{ad} R L x)).\\operatorname{coeff}(\\operatorname{rank} R L) \\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. -/
abbrev IsRegular (x : L) : Prop :=
LieModule.IsRegular R L x