isRegular_def — Mathlib

English

For a fixed basis b, x ∈ L, IsRegular is equivalent to the nonvanishing of the coefficient of the rank-th term in the polyCharpoly associated to ad_R L (or toEnd) with respect to that basis.

Русский

При фиксированном базисе b регулярность элемента x равна ненулевости коэффициента рангового члена в polyCharpoly, связанной с ад-оператором.

LaTeX

$$$$ \\text{IsRegular } R M x \\iff (\\text{polyCharpoly of } (\\operatorname{ad} R L)\\text{ toLinearMap } b).\\operatorname{coeff}(\\operatorname{rank} R L M) \\neq 0 $$$$

Lean4

theorem isRegular_def : IsRegular R M x ↔ (toEnd R L M x).charpoly.coeff (rank R L M) ≠ 0 :=
  Iff.rfl

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