Minimal polynomials of split endomorphisms

If the generalized eigenspaces of an endomorphism f of a finite-dimensional vector space span, then f is annihilated by a power of the product of the linear factors X - C μ over its eigenvalues μ. That product is separable over any field, since its roots are distinct, so this is the input needed to apply Mathlib's Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow without assuming the field is perfect.

Main results

• Module.End.minpoly_dvd_prod_X_sub_C_pow_of_iSup_maxGenEigenspace_eq_top: the minimal polynomial of a split endomorphism divides the finrank-th power of the product of X - C μ over its eigenvalues.

theorem Module.End.minpoly_dvd_prod_X_sub_C_pow_of_iSup_maxGenEigenspace_eq_top {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V} (hf : ⨆ (μ : K), f.maxGenEigenspace μ = ⊤) : minpoly K f ∣ (∏ μ ∈ ⋯.toFinset, (Polynomial.X - Polynomial.C μ)) ^ finrank K V

If the generalized eigenspaces of f span, then the minimal polynomial of f divides the finrank-th power of the product of X - C μ over the eigenvalues μ of f.