diff --git a/Batteries/Data/Rat.lean b/Batteries/Data/Rat.lean
index 686b74eed3..8045da7952 100644
--- a/Batteries/Data/Rat.lean
+++ b/Batteries/Data/Rat.lean
@@ -1,2 +1,3 @@
 import Batteries.Data.Rat.Basic
+import Batteries.Data.Rat.Float
 import Batteries.Data.Rat.Lemmas
diff --git a/Batteries/Data/Rat/Basic.lean b/Batteries/Data/Rat/Basic.lean
index 01cbd07859..37951fbec6 100644
--- a/Batteries/Data/Rat/Basic.lean
+++ b/Batteries/Data/Rat/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Batteries.Data.Nat.Gcd
-import Batteries.Lean.Float
 
 /-! # Basics for the Rational Numbers -/
 
@@ -278,18 +277,4 @@ protected def ceil (a : Rat) : Int :=
   else
     a.num / a.den + 1
 
-/-- Convert this rational number to a `Float` value. -/
-protected def toFloat (a : Rat) : Float := a.num.divFloat a.den
-
-/-- Convert this floating point number to a rational value. -/
-protected def _root_.Float.toRat? (a : Float) : Option Rat :=
-  a.toRatParts.map fun (v, exp) =>
-    mkRat (v.sign * v.natAbs <<< exp.toNat) (1 <<< (-exp).toNat)
-
-/--
-Convert this floating point number to a rational value,
-mapping non-finite values (`inf`, `-inf`, `nan`) to 0.
--/
-protected def _root_.Float.toRat0 (a : Float) : Rat := a.toRat?.getD 0
-
-instance : Coe Rat Float := ⟨Rat.toFloat⟩
+end Rat
diff --git a/Batteries/Data/Rat/Float.lean b/Batteries/Data/Rat/Float.lean
new file mode 100644
index 0000000000..271a6b40fb
--- /dev/null
+++ b/Batteries/Data/Rat/Float.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Batteries.Data.Rat.Basic
+import Batteries.Lean.Float
+
+/-! # Rational Numbers and Float -/
+
+namespace Rat
+
+/-- Convert this rational number to a `Float` value. -/
+protected def toFloat (a : Rat) : Float := a.num.divFloat a.den
+
+/-- Convert this floating point number to a rational value. -/
+protected def _root_.Float.toRat? (a : Float) : Option Rat :=
+  a.toRatParts.map fun (v, exp) =>
+    mkRat (v.sign * v.natAbs <<< exp.toNat) (1 <<< (-exp).toNat)
+
+/--
+Convert this floating point number to a rational value,
+mapping non-finite values (`inf`, `-inf`, `nan`) to 0.
+-/
+protected def _root_.Float.toRat0 (a : Float) : Rat := a.toRat?.getD 0
+
+instance : Coe Rat Float := ⟨Rat.toFloat⟩
+
+end Rat