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