summaryrefslogtreecommitdiff
path: root/Everything.agda
diff options
context:
space:
mode:
authorGreg Brown <greg.brown@cl.cam.ac.uk>2022-04-02 13:34:28 +0100
committerGreg Brown <greg.brown@cl.cam.ac.uk>2022-04-02 13:45:41 +0100
commitefdd7c70a8605c51b7aaa1b0b33914ca741ffe39 (patch)
treebe2cbeed127a6703d166081158fceafee5237ff6 /Everything.agda
parent2167866c53aa7f9cbb52e776bfb64f53acf3fa2c (diff)
Add properties of almost groups.
Diffstat (limited to 'Everything.agda')
-rw-r--r--Everything.agda3
1 files changed, 3 insertions, 0 deletions
diff --git a/Everything.agda b/Everything.agda
index 3c60792..87541c3 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -69,6 +69,9 @@ import Helium.Algebra.Ordered.StrictTotal.Properties.Semigroup
-- operations, etc.)
import Helium.Algebra.Ordered.StrictTotal.Structures
+-- Properties of almost groups
+import Helium.Algebra.Properties.AlmostGroup
+
-- Some more algebraic structures
import Helium.Algebra.Structures