isRegular_iff_coeff_polyCharpoly_rank_ne_zero

English

For DecidableEq ι, IsRegular R M x is equivalent to the evaluation of a polynomial at b.repr x being nonzero.

Русский

При DecidableEq ι регулярность IsRegular R M x эквивалентна ненулевому значению полинома при подстановке b.repr x.

LaTeX

$$$$ \\text{IsRegular } R M x \\iff \\operatorname{MvPolynomial}.eval \\left( b.\\mathrm{repr} \\; x \\right) \\left( (\\operatorname{polyCharpoly} \\phi b).\\operatorname{coeff}(\\operatorname{rank} R L M) \\right) \\neq 0 $$$$

Lean4

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

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