diff --git a/Mathlib/RingTheory/Finiteness/Defs.lean b/Mathlib/RingTheory/Finiteness/Defs.lean
index 289071d1c7064..a56606fa8c8e9 100644
--- a/Mathlib/RingTheory/Finiteness/Defs.lean
+++ b/Mathlib/RingTheory/Finiteness/Defs.lean
@@ -100,7 +100,7 @@ section ModuleAndAlgebra
 
 variable (R A B M N : Type*)
 
-/-- A module over a semiring is `Finite` if it is finitely generated as a module. -/
+/-- A module over a semiring is `Module.Finite` if it is finitely generated as a module. -/
 protected class Module.Finite [Semiring R] [AddCommMonoid M] [Module R M] : Prop where
   out : (⊤ : Submodule R M).FG
 
@@ -142,7 +142,7 @@ namespace RingHom
 
 variable {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
 
-/-- A ring morphism `A →+* B` is `Finite` if `B` is finitely generated as `A`-module. -/
+/-- A ring morphism `A →+* B` is `RingHom.Finite` if `B` is finitely generated as `A`-module. -/
 @[algebraize Module.Finite]
 def Finite (f : A →+* B) : Prop :=
   letI : Algebra A B := f.toAlgebra