isRegular_iff_coeff_polyCharpoly_rank_ne_zero

English

Regularity of x is equivalent to the nonvanishing of the rank-th coefficient of the characteristic polynomial of the endomorphism ad_R L x.

Русский

Регулярность элемента x эквивалентна ненулевому коэффициенту порядка rank в характерном многочлене эндоморфизма ad_R L x.

LaTeX

$$$$ \\text{IsRegular } R M x \\iff (\\operatorname{toEnd} R L M x).\\operatorname{charpoly}.\\operatorname{coeff}(\\operatorname{rank} R L M) \\neq 0 $$$$

Lean4

theorem isRegular_iff_coeff_polyCharpoly_rank_ne_zero [DecidableEq ι] :
    IsRegular R M x ↔ MvPolynomial.eval (b.repr x) ((polyCharpoly φ b).coeff (rank R L M)) ≠ 0 :=
  LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero _ _ _

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