chore(RingTheory/Localization/Basic): split off Defs (#17735)

This PR splits off a `RingTheory.Localization.Defs` file that is supposed to contain the definition of `IsLocalization` and the ring structure on `Localization`, and some basic results that don't need further imports. I am quite sure that we can minimize the transitive imports a bit further but this seems like a decent point to stop for now.



Co-authored-by: Kim Morrison <kim@tqft.net>

Author: Vierkantor

Mathlib.lean

@@ -4000,6 +4000,7 @@ import Mathlib.RingTheory.Localization.Away.Lemmas
 import Mathlib.RingTheory.Localization.BaseChange
 import Mathlib.RingTheory.Localization.Basic
 import Mathlib.RingTheory.Localization.Cardinality
+import Mathlib.RingTheory.Localization.Defs
 import Mathlib.RingTheory.Localization.Finiteness
 import Mathlib.RingTheory.Localization.FractionRing
 import Mathlib.RingTheory.Localization.Ideal

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, Jujian Zhang
 -/
 import Mathlib.Algebra.Algebra.Bilinear
-import Mathlib.RingTheory.Localization.Basic
 import Mathlib.Algebra.Exact
+import Mathlib.Algebra.Algebra.Tower
+import Mathlib.RingTheory.Localization.Defs
 
 /-!
 # Localized Module

Mathlib/Algebra/Polynomial/Laurent.lean

@@ -6,7 +6,7 @@ Authors: Damiano Testa
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Reverse
 import Mathlib.Algebra.Polynomial.Inductions
-import Mathlib.RingTheory.Localization.Basic
+import Mathlib.RingTheory.Localization.Defs
 
 /-!  # Laurent polynomials