isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank

English

IsNilRegular x is equivalent to the natTrailingDegree of φ x's charpoly equalling nilRank φ.

Русский

IsNilRegular x эквивалентно тому, что natTrailingDegree характеристического полинома φ x равен nilRank φ.

LaTeX

$$IsNilRegular φ x ↔ (φ x).charpoly.natTrailingDegree = nilRank φ$$

Lean4

theorem isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank [Nontrivial R] :
    IsNilRegular φ x ↔ (φ x).charpoly.natTrailingDegree = nilRank φ :=
  by
  rw [isNilRegular_def]
  constructor
  · intro h
    exact le_antisymm (Polynomial.natTrailingDegree_le_of_ne_zero h) (nilRank_le_natTrailingDegree_charpoly φ x)
  · intro h
    rw [← h]
    apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr
    apply (LinearMap.charpoly_monic _).ne_zero

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