Theorems · Definition · group theory
commutator
(G : Type u_1) → [inst : Group G] → Subgroup G
The commutator subgroup of a group G is the normal subgroup
generated by the commutators [p,q] = p * q * p⁻¹ * q⁻¹.
- Defined in
- Mathlib.GroupTheory.Commutator.Basic
- Cited by
- 56 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topproof · cited by 9,680
- Groupstatement and proof · cited by 6,238
- Subgroupstatement · cited by 3,593
- Bracket.bracketproof · cited by 642
Cited by61
Results whose statement or proof uses this declaration.
- Abelianizationproof · cited by 32
- Abelianization.liftproof · cited by 9
- commutator_eq_closurestatement · cited by 7
- Subgroup.map_subtype_commutatorstatement · cited by 7
- commutator_defstatement · cited by 6
- Abelianization.commutator_subset_kerstatement · cited by 5
- Group.IsPerfect.commutator_eq_topstatement · cited by 5
- MulAction.IwasawaStructure.commutator_lestatement · cited by 4
- Group.IsSolvable.commutator_lt_top_of_nontrivialstatement and proof · cited by 3
- commutator_alternatingGroup_eq_topstatement and proof · cited by 3
- Group.isPerfect_defstatement and proof · cited by 2
- commutator_eq_bot_iff_center_eq_topstatement · cited by 2