feat: port Topology.Algebra.Group.Basic (#2267)

Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Feb 21, 2023 · e7e49c8 · e7e49c8
1 parent f327ca8
commit e7e49c8
Show file tree

Hide file tree

Showing 3 changed files with 2,014 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1129,6 +1129,7 @@ import Mathlib.Testing.SlimCheck.Testable
 import Mathlib.Topology.Alexandroff
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions
+import Mathlib.Topology.Algebra.Group.Basic
 import Mathlib.Topology.Algebra.GroupWithZero
 import Mathlib.Topology.Algebra.Monoid
 import Mathlib.Topology.Algebra.MulAction