feat: port RingTheory.FractionalIdeal (#4243)

leanprover-community · May 23, 2023 · 6c2856c · 6c2856c
1 parent dcfe638
commit 6c2856c
Show file tree

Hide file tree

Showing 2 changed files with 1,634 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1935,6 +1935,7 @@ import Mathlib.RingTheory.FiniteType
 import Mathlib.RingTheory.Finiteness
 import Mathlib.RingTheory.Fintype
 import Mathlib.RingTheory.Flat
+import Mathlib.RingTheory.FractionalIdeal
 import Mathlib.RingTheory.FreeCommRing
 import Mathlib.RingTheory.FreeRing
 import Mathlib.RingTheory.GradedAlgebra.Basic