English
Equality between coefficient-zero statements holds across bases: (polyCharpoly φ b).coeff k = 0 iff (polyCharpoly φ b').coeff k = 0.
Русский
Суждения о равенстве нулю коэффициента k-го полинома сохраняются между базисами: (polyCharpoly φ b).coeff k = 0 тогда и только тогда, когда (polyCharpoly φ b').coeff k = 0.
LaTeX
$$((\mathrm{polyCharpoly } φ b).\mathrm{coeff} k) = 0 \iff ((\mathrm{polyCharpoly } φ b').\mathrm{coeff} k) = 0$$
Lean4
/-- 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.nilRank φ 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 `LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree`. -/
noncomputable def nilRank (φ : L →ₗ[R] Module.End R M) : ℕ :=
nilRankAux φ (Module.Free.chooseBasis R L)
