From 1afedcdbc501ef47d53e9ebd8c3d41f4f964c51c Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Thu, 27 Jun 2024 22:18:39 -0400 Subject: [PATCH] minor --- src/ring_theory/localization/submodule.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ring_theory/localization/submodule.lean b/src/ring_theory/localization/submodule.lean index ffe41ebd8441f..3b3b3137f3b35 100644 --- 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