Commit 2023-06-10 05:46 90dafad1

View on Github →

feat: port LinearAlgebra.Eigenspace.IsAlgClosed (#4943)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Eigenspace/IsAlgClosed.lean

added theorem Module.End.exists_eigenvalue

added theorem Module.End.iSup_generalizedEigenspace_eq_top