update module docstring

mattrobball · mattrobball · commit 51253bc51cce · 2024-08-16T09:58:56.000-04:00
diff --git a/Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean b/Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
@@ -12,7 +12,9 @@ import Mathlib.Init.Data.Int.Order
 # The rational numbers possess a linear order
 
 This file constructs the order on `ℚ` and proves various facts relating the order to
-ring structure on `ℚ`.
+ring structure on `ℚ`. This only used unbundled type classes relating the order structure
+and algebra structure on `ℚ`. For the bundled `LinearOrderedCommRing` instance on `Q`,
+see `Algebra.Order.Ring.Rat`.
 
 ## Tags
 
