Commit 2024-02-01 05:56 2e5fa833

View on Github →

feat: a supremum of semisimple modules is semisimple (#10086) Another small step toward Jordan-Chevalley-Dunford.

Estimated changes

Modified Mathlib/LinearAlgebra/Basic.lean

added theorem Submodule.map_comap_eq_of_le

Modified Mathlib/Order/CompleteLattice.lean

added theorem biInf_congr'

added theorem biInf_le

added theorem biSup_congr'

added theorem le_biSup

Modified Mathlib/Order/CompleteLatticeIntervals.lean

added theorem Set.Iic.coe_biInf

added theorem Set.Iic.coe_biSup

added theorem Set.Iic.coe_iInf

added theorem Set.Iic.coe_iSup

added theorem Set.Iic.coe_sInf

added theorem Set.Iic.coe_sSup

added theorem Set.Iic.isCompactElement

added theorem complementedLattice_of_complementedLattice_Iic

Modified Mathlib/Order/Disjoint.lean

Modified Mathlib/RingTheory/SimpleModule.lean

added theorem isSemisimpleModule_biSup_of_IsSemisimpleModule_submodule

added theorem isSemisimpleModule_of_IsSemisimpleModule_submodule'

added theorem isSemisimpleModule_of_IsSemisimpleModule_submodule