Typo in Data.Rat.Sqrt (#1577)

Just noticed a small typo from when I ported `Data.Rat.Sqrt`
leanprover-community · Jan 15, 2023 · 314c3c7 · 314c3c7
1 parent 38edbb8
commit 314c3c7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Data/Rat/Sqrt.lean b/Mathlib/Data/Rat/Sqrt.lean
@@ -15,7 +15,7 @@ import Mathlib.Data.Int.Sqrt
 /-!
 # Square root on rational numbers
 
-This file defines the square root function on rational numbers `rat.sqrt`
+This file defines the square root function on rational numbers `Rat.sqrt`
 and proves several theorems about it.
 
 -/