Skip to content

Commit

Permalink
docs(RingTheory/Finiteness/Defs): specify namespace of Finite (#19359)
Browse files Browse the repository at this point in the history
Currently, `Module.Finite` and `RingHom.Finite` have docstrings that link to `Finite`, which is confusing.
  • Loading branch information
winstonyin committed Nov 22, 2024
1 parent 1a2513a commit d511775
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/RingTheory/Finiteness/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down

0 comments on commit d511775

Please sign in to comment.