Theorems · Inductive type · group theory
IsSimpleAddGroup
(A : Type u_2) → [AddGroup A] → Prop
An AddGroup is simple when it has exactly two normal AddSubgroups.
- Defined in
- Mathlib.GroupTheory.Subgroup.Simple
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement · cited by 4,410
Cited by16
Results whose statement or proof uses this declaration.
- AddSubgroup.Normal.eq_bot_or_eq_topstatement and proof · cited by 3
- IsSimpleAddGroup.prime_cardstatement and proof · cited by 2
- AddSubgroup.IsSubnormal.normal_of_isSimpleAddGroupstatement and proof · cited by 1
- IsSimpleAddGroup.casesOnstatement and proof · cited by 1
- IsSimpleAddGroup.eq_bot_or_eq_top_of_normalstatement and proof · cited by 1
- IsSimpleAddGroup.isSimpleAddGroup_of_surjectivestatement and proof · cited by 1
- isSimpleAddGroup_iffstatement and proof · cited by 1
- isSimpleAddGroup_of_prime_cardstatement · cited by 1
- AddEquiv.isSimpleAddGroupstatement and proof · cited by 1
- AddGroup.is_simple_iff_prime_cardstatement and proof · cited by 1
- AddSubgroup.IsSubnormal.eq_bot_or_top_of_isSimpleAddGroupstatement and proof · cited by 0
- IsSimpleAddGroup.finitestatement and proof · cited by 0