From d511775f5a2ce12b2d54913c5f9ffdc0457bb663 Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Fri, 22 Nov 2024 10:20:47 +0000 Subject: [PATCH] docs(RingTheory/Finiteness/Defs): specify namespace of `Finite` (#19359) Currently, `Module.Finite` and `RingHom.Finite` have docstrings that link to `Finite`, which is confusing. --- Mathlib/RingTheory/Finiteness/Defs.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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