From 5fb990fcbd8d56e61e4276adcbe6deb19b5d7c64 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Fri, 28 Mar 2025 10:56:44 -0400 Subject: [PATCH] doc: Rat.lean docstring: "Mathlib" -> "Batteries" (#7708) This PR fixes an inaccuracy in a module doc for an internal file. The "Mathib rational numbers" are actually defined in Batteries now - someone using Batteries but not Mathlib could potentialy be misled by this. I think this is an improvement on the docstring. --- src/Std/Internal/Rat.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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