English
NilRankAux φ b is defined as the smallest index where polyCharpoly φ b has a nonzero coefficient; this index is independent of the basis, up to equality with natTrailingDegree.
Русский
NilRankAux φ b — это наименьший индекс, при котором polyCharpoly φ b имеет ненулевой коэффициент; этот индекс не зависит от базиса (сопоставим с natTrailingDegree).
LaTeX
$$nilRankAux φ b = (polyCharpoly φ b).natTrailingDegree$$
Lean4
/-- (Implementation detail, see `LinearMap.nilRank`.)
Let `L` and `M` be finite free modules over `R`,
and let `φ : L →ₗ[R] Module.End R M` be a linear family of endomorphisms.
Then `LinearMap.nilRankAux φ b` is the smallest index
at which `LinearMap.polyCharpoly φ b` has a non-zero coefficient.
This number does not depend on the choice of `b`, see `nilRankAux_basis_indep`. -/
noncomputable def nilRankAux (φ : L →ₗ[R] Module.End R M) (b : Basis ι R L) : ℕ :=
(polyCharpoly φ b).natTrailingDegree
