Commit 2023-11-27 21:37 3c30dbb2

View on Github →

feat: a family of generalized eigenvalues for a commuting linear family of endomorphims must be linear (#8656)

Estimated changes

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.iSup_generalizedEigenspace_inf_le_add

added theorem Module.End.iSup_generalizedEigenspace_le_smul

added theorem Module.End.map_add_of_iInf_generalizedEigenspace_ne_bot_of_commute

added theorem Module.End.map_smul_of_iInf_generalizedEigenspace_ne_bot