chore: fix docstring of IsLocalization (#7234)

leanprover-community · Sep 18, 2023 · 00fdd1f · 00fdd1f
1 parent 3882a68
commit 00fdd1f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/Localization/Basic.lean b/Mathlib/RingTheory/Localization/Basic.lean
@@ -94,7 +94,7 @@ variable {R : Type*} [CommSemiring R] (M : Submonoid R) (S : Type*) [CommSemirin
 
 variable [Algebra R S] {P : Type*} [CommSemiring P]
 
-/-- The typeclass `IsLocalization (M : Submodule R) S` where `S` is an `R`-algebra
+/-- The typeclass `IsLocalization (M : Submonoid R) S` where `S` is an `R`-algebra
 expresses that `S` is isomorphic to the localization of `R` at `M`. -/
 class IsLocalization : Prop where
   --Porting note: add ' to fields, and made new versions of these with either `S` or `M` explicit.