mathlib

a83230e0 - feat(linear_algebra/eigenspace): define the maximal generalized eigenspace (#7125)

feat(linear_algebra/eigenspace): define the maximal generalized eigenspace (#7125) And prove that it is of the form kernel of `(f - μ • id) ^ k` for some finite `k` for endomorphisms of Noetherian modules.