Theorems · Inductive type · group theory
Group.IsPerfect
(G : Type u_1) → [Group G] → Prop
A group G is perfect if G equals its commutator subgroup ⁅G, G⁆.
- Defined in
- Mathlib.GroupTheory.IsPerfect
- Cited by
- 17 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 by19
Results whose statement or proof uses this declaration.
- Group.IsPerfect.commutator_eq_topstatement and proof · cited by 5
- Subgroup.isPerfect_iffstatement · cited by 2
- Group.isPerfect_defstatement and proof · cited by 2
- Group.IsPerfect.not_isSolvablestatement and proof · cited by 2
- SL2Simple.PSL_commutator_eq_topproof · cited by 1
- Subgroup.commutator_eq_selfstatement and proof · cited by 1
- Group.IsPerfect.mapstatement and proof · cited by 1
- Group.IsPerfect.rangestatement and proof · cited by 1
- Group.IsPerfect.top_iffstatement and proof · cited by 1
- Group.IsPerfect.upperCentralSeries_eq_centerstatement and proof · cited by 1
- Group.IsPerfect.casesOnstatement and proof · cited by 0
- Group.IsPerfect.center_quotient_center_eq_botstatement and proof · cited by 0