Simplicity of quotient groups

This file characterizes when a quotient group is simple.

Main results

• CommGroup.isSimpleGroup_iff_isCoatom: a subgroup of a commutative group is a coatom in the subgroup lattice iff the quotient by it is simple.

theorem CommGroup.isSimpleGroup_iff_isCoatom {G : Type u_1} [CommGroup G] {M : Subgroup G} : IsSimpleGroup (G ⧸ M) ↔ IsCoatom M

A subgroup of a commutative group is maximal (a coatom in the subgroup lattice) iff the quotient by it is simple. Group analogue of isSimpleModule_iff_isCoatom.

theorem AddCommGroup.isSimpleAddGroup_iff_isCoatom {G : Type u_1} [AddCommGroup G] {M : AddSubgroup G} : IsSimpleAddGroup (G ⧸ M) ↔ IsCoatom M

A subgroup of an additive commutative group is maximal (a coatom in the subgroup lattice) iff the quotient by it is simple. Additive group analogue of isSimpleModule_iff_isCoatom.