docs(RingTheory/Localization/FractionRing): mention total fraction ri…

…ng in docstring (#5827)
leanprover-community · Jul 12, 2023 · 5149cfa · 5149cfa
1 parent 806f7f9
commit 5149cfa
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -284,6 +284,8 @@ variable (A)
 
 We instantiate this definition as generally as possible, and assume that the
 commutative ring `R` is an integral domain only when this is needed for proving.
+
+In this generality, this construction is also known as the *total fraction ring* of `R`.
 -/
 @[reducible]
 def FractionRing :=