minor

leanprover-community · Jun 28, 2024 · 1afedcd · 1afedcd
1 parent 2bbad5e
commit 1afedcd
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/ring_theory/localization/submodule.lean b/src/ring_theory/localization/submodule.lean
@@ -18,8 +18,8 @@ See `src/ring_theory/localization/basic.lean` for a design overview.
 localization, ring localization, commutative ring localization, characteristic predicate,
 commutative ring, field of fractions
 -/
-variables {R : Type*} [comm_ring R] (M : submonoid R) (S : Type*) [comm_ring S]
-variables [algebra R S] {P : Type*} [comm_ring P]
+variables {R : Type*} [comm_semiring R] (M : submonoid R) (S : Type*) [comm_semiring S]
+variables [algebra R S] {P : Type*} [comm_semiring P]
 
 namespace is_localization