Commit 2021-04-10 14:43 a83230e0

View on Github →

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.

Estimated changes

Modified src/linear_algebra/eigenspace.lean

modified theorem module.End.eigenspace_le_generalized_eigenspace

modified def module.End.generalized_eigenspace

deleted theorem module.End.generalized_eigenspace_mono

added def module.End.maximal_generalized_eigenspace

added theorem module.End.maximal_generalized_eigenspace_eq

Modified src/order/order_iso_nat.lean

added theorem well_founded.supr_eq_monotonic_sequence_limit