feat: port RingTheory.LocalProperties (#5010)

Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
leanprover-community · Jun 15, 2023 · 00b77c0 · 00b77c0
1 parent 51a5ef1
commit 00b77c0
Show file tree

Hide file tree

Showing 2 changed files with 653 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2470,6 +2470,7 @@ import Mathlib.RingTheory.IntegrallyClosed
 import Mathlib.RingTheory.IsTensorProduct
 import Mathlib.RingTheory.JacobsonIdeal
 import Mathlib.RingTheory.LaurentSeries
+import Mathlib.RingTheory.LocalProperties
 import Mathlib.RingTheory.Localization.AsSubring
 import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.RingTheory.Localization.Away.AdjoinRoot