feat: port Topology.Algebra.OpenSubgroup (#2889)

leanprover-community · Mar 17, 2023 · f4d2505 · f4d2505
1 parent 81530d1
commit f4d2505
Show file tree

Hide file tree

Showing 2 changed files with 395 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1423,6 +1423,7 @@ import Mathlib.Topology.Algebra.InfiniteSum.Ring
 import Mathlib.Topology.Algebra.Localization
 import Mathlib.Topology.Algebra.Monoid
 import Mathlib.Topology.Algebra.MulAction
+import Mathlib.Topology.Algebra.OpenSubgroup
 import Mathlib.Topology.Algebra.Order.Archimedean
 import Mathlib.Topology.Algebra.Order.Compact
 import Mathlib.Topology.Algebra.Order.ExtendFrom