Commit 2024-10-15 03:55 9958ee4c
View on Github →chore(GroupTheory/Congruence/Basic): split off Defs
and Hom
(#17729)
GroupTheory.Congruence.Defs
sets up the quotient and its monoid structure, and its imports and contents are trimmed down to the minimum to make that possible.
GroupTheory.Congruence.Hom
are those results that couldn't go into GroupTheory.Congruence.Defs
but can be added after we import monoid homs.