feat: port GroupTheory.FreeAbelianGroup (#2247)

Co-authored-by: David Renshaw <dwrenshaw@gmail.com>
leanprover-community · Mar 14, 2023 · 0eb2381 · 0eb2381
1 parent 83941ae
commit 0eb2381
Show file tree

Hide file tree

Showing 2 changed files with 619 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -942,6 +942,7 @@ import Mathlib.GroupTheory.Divisible
 import Mathlib.GroupTheory.DoubleCoset
 import Mathlib.GroupTheory.EckmannHilton
 import Mathlib.GroupTheory.Finiteness
+import Mathlib.GroupTheory.FreeAbelianGroup
 import Mathlib.GroupTheory.FreeGroup
 import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.BigOperators