isRegular_iff_natTrailingDegree_charpoly_eq_rank

English

For a fixed basis b of L, regularity is equivalent to the nonvanishing of the coefficient at rank in the polyCharpoly of ad_R L.

Русский

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

LaTeX

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

Lean4

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

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