feat: port Deprecated.Subgroup (#1876)

leanprover-community · Jan 27, 2023 · 5ed72b2 · 5ed72b2
1 parent f57e271
commit 5ed72b2
Show file tree

Hide file tree

Showing 2 changed files with 778 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -547,6 +547,7 @@ import Mathlib.Data.W.Basic
 import Mathlib.Data.ZMod.Defs
 import Mathlib.Deprecated.Group
 import Mathlib.Deprecated.Ring
+import Mathlib.Deprecated.Subgroup
 import Mathlib.Deprecated.Submonoid
 import Mathlib.Dynamics.FixedPoints.Basic
 import Mathlib.GroupTheory.Archimedean