Mathlib Changelog
v4
Changelog
About
Github
Theorem
Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo
Modification history
2024-10-01 22:14
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
feat: a family of compatible triangularisable endomorphisms are simultaneously triangularisable (#17194)
Added
Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo
View on Github →