Theorems · Inductive type · group theory
IsSimpleGroup
(G : Type u_1) → [Group G] → Prop
A Group is simple when it has exactly two normal Subgroups.
- Defined in
- Mathlib.GroupTheory.Subgroup.Simple
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Group
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.
- Groupstatement · cited by 6,238
Cited by28
Results whose statement or proof uses this declaration.
- Subgroup.Normal.eq_bot_or_eq_topstatement and proof · cited by 7
- IsSimpleGroup.prime_cardstatement and proof · cited by 3
- alternatingGroup.isSimpleGroupstatement · cited by 3
- Matrix.ProjectiveSpecialLinearGroup.rank_two_simple'statement · cited by 1
- IsSimpleGroup.casesOnstatement and proof · cited by 1
- IsSimpleGroup.derivedSeries_succstatement and proof · cited by 1
- IsSimpleGroup.eq_bot_or_eq_top_of_normalstatement and proof · cited by 1
- IsSimpleGroup.isSimpleGroup_of_surjectivestatement and proof · cited by 1
- MulEquiv.isSimpleGroupstatement and proof · cited by 1
- isSimpleGroup_iffstatement and proof · cited by 1
- Group.is_simple_iff_prime_cardstatement and proof · cited by 1
- isSimpleGroup_of_prime_cardstatement · cited by 1