feat: port GroupTheory.Exponent (#4313)

leanprover-community · May 25, 2023 · f85a2b8 · f85a2b8
1 parent c8442dc
commit f85a2b8
Show file tree

Hide file tree

Showing 2 changed files with 393 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1479,6 +1479,7 @@ import Mathlib.GroupTheory.Coset
 import Mathlib.GroupTheory.Divisible
 import Mathlib.GroupTheory.DoubleCoset
 import Mathlib.GroupTheory.EckmannHilton
+import Mathlib.GroupTheory.Exponent
 import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.FreeAbelianGroup
 import Mathlib.GroupTheory.FreeAbelianGroupFinsupp