Theorems · Definition · group theory
Subgroup.center
(G : Type u_1) → [inst : Group G] → Subgroup G
The center of a group G is the set of elements that commute with everything in G
- Defined in
- Mathlib.GroupTheory.Subgroup.Center
- Cited by
- 121 results in Mathlib
- Foundations
- Depth 19 from the axioms, rests on 125 definitions · 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.
- Groupstatement and proof · cited by 6,238
- Subgroupstatement · cited by 3,593
- Submonoidproof · cited by 3,086
- Submonoid.centerproof · cited by 24
Cited by144
Results whose statement or proof uses this declaration.
- Matrix.ProjGenLinGroupproof · cited by 23
- Matrix.ProjGenLinGroup.mkproof · cited by 19
- Subgroup.mem_center_iffstatement and proof · cited by 10
- Matrix.ProjectiveSpecialLinearGroupproof · cited by 9
- Subgroup.upperCentralSeries_onestatement · cited by 7
- SpecialLinearGroup.centerEquivRootsOfUnitystatement and proof · cited by 6
- Matrix.GeneralLinearGroup.center_eq_range_scalarstatement and proof · cited by 6
- Subgroup.center_eq_top_iffstatement and proof · cited by 4
- Matrix.ProjectiveSpecialLinearGroup.toPGLstatement and proof · cited by 4
- Subgroup.centerCongrstatement · cited by 3
- MonoidHom.transferCenterPowstatement and proof · cited by 3
- Subgroup.centralizer_eq_top_iff_subsetstatement · cited by 3