IsRegular — Mathlib

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

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