Commit 2024-10-01 22:14 9e4a4bef

View on Github →

feat: a family of compatible triangularisable endomorphisms are simultaneously triangularisable (#17194)

Estimated changes

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

added theorem Submodule.inf_iInf

Modified Mathlib/Algebra/Module/Submodule/LinearMap.lean

added theorem LinearMap.restrict_smul_one

Modified Mathlib/Algebra/Module/Submodule/Map.lean

added theorem Submodule.map_iInf

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq

added theorem Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo

added theorem Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

added theorem Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo