Structures · Algebra
IsSimpleAddGroup
An AddGroup is simple when it has exactly two normal AddSubgroups.
- Defined in
- Mathlib.GroupTheory.Subgroup.Simple
- Shape
- One type argument · adds eq_bot_or_eq_top_of_normal
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- ZMod
How is a type an instance?
Loading the hierarchy index…
Assumed by9
- AddSubgroup.Normal.eq_bot_or_eq_top
- IsSimpleAddGroup.prime_card
- AddEquiv.isSimpleAddGroup
- IsSimpleAddGroup.eq_bot_or_eq_top_of_normal
- IsSimpleAddGroup.isSimpleAddGroup_of_surjective
- IsSimpleAddGroup.instIsSimpleOrderAddSubgroup
- IsSimpleAddGroup.isAddCyclic
- IsSimpleAddGroup.finite
- IsSimpleAddGroup.toNontrivial