nilRank_le_card — Mathlib

English

NilRank φ equals the natTrailingDegree of polyCharpoly φ b for any basis b.

Русский

NilRank φ равно natTrailingDegree polyCharpoly φ b для любого базиса b.

LaTeX

$$nilRank φ = (polyCharpoly φ b).natTrailingDegree$$

Lean4

theorem nilRank_le_card {ι : Type*} [Fintype ι] (b : Basis ι R M) : nilRank φ ≤ Fintype.card ι :=
  by
  apply Polynomial.natTrailingDegree_le_of_ne_zero
  rw [← Module.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L), Polynomial.coeff_natDegree,
    (polyCharpoly_monic _ _).leadingCoeff]
  apply one_ne_zero

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