Def Group.commGroupOfCenterEqTop

Modification history

2024-04-20 06:50

Mathlib/GroupTheory/Subgroup/Basic.lean

chore: refactor to avoid importing Ring for Group topics (#11913) …

Modified Group.commGroupOfCenterEqTop View on Github →

2023-01-26 10:26

Mathlib/GroupTheory/Subgroup/Basic.lean

feat: port GroupTheory.Subgroup.Basic (#1797)

Added Group.commGroupOfCenterEqTop View on Github →