feat: port RingTheory.Localization.Integral (leanprover-community#4231)

qawbecrdtey · Jun 12, 2023 · 2586500 · 2586500
1 parent 4f96d77
commit 2586500
Show file tree

Hide file tree

Showing 2 changed files with 468 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1953,6 +1953,7 @@ import Mathlib.RingTheory.Localization.Cardinality
 import Mathlib.RingTheory.Localization.FractionRing
 import Mathlib.RingTheory.Localization.Ideal
 import Mathlib.RingTheory.Localization.Integer
+import Mathlib.RingTheory.Localization.Integral
 import Mathlib.RingTheory.Localization.InvSubmonoid
 import Mathlib.RingTheory.Localization.LocalizationLocalization
 import Mathlib.RingTheory.Localization.Module