nilRankAux_le — Mathlib

English

NilRankAux φ b is defined as the trailing degree of polyCharpoly φ b.

Русский

NilRankAux φ b задаётся как нижняя доля степени полинома polyCharpoly φ b.

LaTeX

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

Lean4

theorem nilRankAux_le [Nontrivial R] (b : Basis ι R L) (b' : Basis ι' R L) : nilRankAux φ b ≤ nilRankAux φ b' :=
  by
  apply Polynomial.natTrailingDegree_le_of_ne_zero
  rw [Ne, (polyCharpoly_coeff_eq_zero_iff_of_basis φ b b' _).not]
  apply polyCharpoly_coeff_nilRankAux_ne_zero

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