feat: port Algebra.RingQuot (#3383)

leanprover-community · Apr 21, 2023 · 4bef854 · 4bef854
1 parent 94d947d
commit 4bef854
Show file tree

Hide file tree

Showing 3 changed files with 708 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -276,6 +276,7 @@ import Mathlib.Algebra.Ring.Regular
 import Mathlib.Algebra.Ring.Semiconj
 import Mathlib.Algebra.Ring.ULift
 import Mathlib.Algebra.Ring.Units
+import Mathlib.Algebra.RingQuot
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.Algebra.Squarefree
 import Mathlib.Algebra.Star.Basic