refactor: alternative to agda#2852 and agda#2854

jamesmckinna · jamesmckinna · commit e2ff677ed39c · 2025-11-05T14:10:20.000Z
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -79,6 +79,12 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Construct.Quotient.{Abelian}Group` for the definition of quotient (Abelian) groups.
+
+* `Algebra.Construct.Sub.{Abelian}Group` for the definition of sub-(Abelian)groups.
+
+* `Algebra.Construct.Sub.Group.Normal` for the definition of normal subgroups.
+
 * `Algebra.Properties.BooleanRing`.
 
 * `Algebra.Properties.BooleanSemiring`.
