diff --git a/src/Std/Internal/Rat.lean b/src/Std/Internal/Rat.lean index a71b24d72f..6a109a5f4e 100644 --- a/src/Std/Internal/Rat.lean +++ b/src/Std/Internal/Rat.lean @@ -14,7 +14,7 @@ namespace Internal /-! Rational numbers for implementing decision procedures. - We should not confuse them with the Mathlib rational numbers. + We should not confuse them with the Batteries rational numbers, also used by Mathlib. -/ structure Rat where