feat: Port Deprecated.Group and Deprecated.Ring (#1368)

leanprover-community · Jan 6, 2023 · 6df3ab7 · 6df3ab7
1 parent 667f74a
commit 6df3ab7
Show file tree

Hide file tree

Showing 3 changed files with 624 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -350,6 +350,8 @@ import Mathlib.Data.UInt
 import Mathlib.Data.ULift
 import Mathlib.Data.UnionFind
 import Mathlib.Data.Vector
+import Mathlib.Deprecated.Group
+import Mathlib.Deprecated.Ring
 import Mathlib.Dynamics.FixedPoints.Basic
 import Mathlib.GroupTheory.EckmannHilton
 import Mathlib.GroupTheory.GroupAction.Defs