isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero

English

IsNilRegular φ x is equivalent to the i-th coefficient (nilRank φ) of φ x's charpoly being nonzero.

Русский

IsNilRegular φ x эквивалентно тому, что коэффициент при индексе nilRank φ в характеристическом полиномe φ x ненулевой.

LaTeX

$$IsNilRegular φ x ↔ MvPolynomial.eval (b.repr x) ((polyCharpoly φ b).coeff (nilRank φ)) ≠ 0$$

Lean4

theorem isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero :
    IsNilRegular φ x ↔ MvPolynomial.eval (b.repr x) ((polyCharpoly φ b).coeff (nilRank φ)) ≠ 0 := by
  rw [IsNilRegular, polyCharpoly_coeff_eval]

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