isRegular_iff_natTrailingDegree_charpoly_eq_rank

English

The regularity is equivalent to the nonzero of the coefficient at rank in the nilRank-related polynomial.

Русский

Регулярность эквивалентна ненулевому коэффициенту при ранге в соответствующем полиномe nilRank.

LaTeX

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

Lean4

theorem isRegular_iff_natTrailingDegree_charpoly_eq_rank [Nontrivial R] :
    IsRegular R x ↔ (ad R L x).charpoly.natTrailingDegree = rank R L :=
  LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank _ _

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