Commit 2024-10-17 08:31 c41f54d5

View on Github →

feat: generalise LieModule.independent_genWeightSpace to any family of compatible endomorphisms (#17654) Also create new file to group together results about simultaneous (generalised) eigenspaces.

Estimated changes

Modified Mathlib.lean

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

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

deleted theorem Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq

deleted theorem Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo

Created Mathlib/LinearAlgebra/Eigenspace/Pi.lean

added theorem Module.End.disjoint_iInf_maxGenEigenspace

added theorem Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq

added theorem Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo

added theorem Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo

added theorem Module.End.injOn_iInf_maxGenEigenspace

added theorem Module.End.mem_iInf_maxGenEigenspace_iff

added theorem Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

deleted theorem Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo