feat (RingTheory/Localization/LocalizationLocalization): Generalize f…

…rom CommRing to CommSemiring (#9112)

Change hypothesis CommRing to CommSemiring in the first section of the file

Mathlib/RingTheory/Localization/LocalizationLocalization.lean

@@ -22,17 +22,19 @@ commutative ring, field of fractions
 -/
 
 
-variable {R : Type*} [CommRing R] (M : Submonoid R) {S : Type*} [CommRing S]
-
-variable [Algebra R S] {P : Type*} [CommRing P]
 
 open Function BigOperators
 
 namespace IsLocalization
 
 section LocalizationLocalization
 
-variable (N : Submonoid S) (T : Type*) [CommRing T] [Algebra R T]
+variable {R : Type*} [CommSemiring R] (M : Submonoid R) {S : Type*} [CommSemiring S]
+
+variable [Algebra R S] {P : Type*} [CommSemiring P]
+
+variable (N : Submonoid S) (T : Type*) [CommSemiring T] [Algebra R T]
+
 
 section
 
@@ -254,6 +256,8 @@ end IsLocalization
 
 namespace IsFractionRing
 
+variable {R : Type*} [CommRing R] (M : Submonoid R) {S : Type*} [CommRing S]
+
 open IsLocalization
 
 theorem isFractionRing_of_isLocalization (S T : Type*) [CommRing S] [CommRing T] [Algebra R S]