Skip to content

Commit f4d2505

Browse files
committed
feat: port Topology.Algebra.OpenSubgroup (#2889)
1 parent 81530d1 commit f4d2505

File tree

2 files changed

+395
-0
lines changed

2 files changed

+395
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1423,6 +1423,7 @@ import Mathlib.Topology.Algebra.InfiniteSum.Ring
14231423
import Mathlib.Topology.Algebra.Localization
14241424
import Mathlib.Topology.Algebra.Monoid
14251425
import Mathlib.Topology.Algebra.MulAction
1426+
import Mathlib.Topology.Algebra.OpenSubgroup
14261427
import Mathlib.Topology.Algebra.Order.Archimedean
14271428
import Mathlib.Topology.Algebra.Order.Compact
14281429
import Mathlib.Topology.Algebra.Order.ExtendFrom

0 commit comments

Comments
 (0)