Mathlib: finite-order endomorphism with one eigenvalue is scalar (semisimple+nilpotent)

To show f : End ℂ V with f^N = 1 and all charpoly roots equal to c is algebraMap ℂ _ c: (1) Splits.eq_prod_roots_of_monic (LinearMap.charpoly_monic f) plus Multiset.eq_replicate (card via Splits.natDegree_eq_card_roots and LinearMap.charpoly_natDegree) gives charpoly = (X - C c)^d; LinearMap.aeval_self_charpoly then gives IsNilpotent (f - algebraMap c) after simpa. (2) Module.End.isSemisimple_of_squarefree_aeval_eq_zero (p := X^N - C 1) with (separable_X_pow_sub_C 1 _ one_ne_zero).squarefree. (3) eq_zero_of_isNilpotent_isSemisimple hnil (isSemisimple_sub_algebraMap_iff.2 hss). About 20 lines, no diagonalization needed. Also: eigenvalues of ρ g are roots of unity — copy the proof of Representation.isIntegral_character (hasEigenvalue_iff_isRoot_charpoly + smul_left_injective).