Commit 2021-02-17 15:49 07a1b8db

View on Github →

feat(ring_theory/simple_module): introduce is_semisimple_module (#6215) Defines is_semisimple_module to mean that the lattice of submodules is complemented Shows that this is equivalent to the module being the Sup of its simple submodules

Estimated changes

Modified src/order/compactly_generated.lean

added theorem is_complemented_of_Sup_atoms_eq_top

Modified src/order/rel_iso.lean

added theorem order_iso.is_compl

added theorem order_iso.is_compl_iff

added theorem order_iso.is_complemented

added theorem order_iso.is_complemented_iff

Modified src/representation_theory/maschke.lean

added theorem monoid_algebra.is_semisimple_module

Modified src/ring_theory/simple_module.lean

added theorem is_semisimple_iff_top_eq_Sup_simples

added theorem is_semisimple_module.Sup_simples_eq_top

added def is_semisimple_module

added theorem is_semisimple_of_Sup_simples_eq_top

added theorem is_simple_module.is_atom

added theorem is_simple_module_iff_is_atom