feat: port RingTheory.Ideal.Quotient (#2412)

Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com> Co-authored-by: Yury Kudryashov <urkud@urkud.name> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
leanprover-community · Mar 9, 2023 · 43fb515 · 43fb515
1 parent f863c3c
commit 43fb515
Show file tree

Hide file tree

Showing 2 changed files with 523 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1159,6 +1159,7 @@ import Mathlib.RingTheory.Coprime.Lemmas
 import Mathlib.RingTheory.Fintype
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.NonZeroDivisors
 import Mathlib.RingTheory.OreLocalization.Basic
 import Mathlib.RingTheory.OreLocalization.OreSet