diff --git a/Batteries/Data/Rat/Basic.lean b/Batteries/Data/Rat/Basic.lean
index e4b95d4106..600e67981f 100644
--- a/Batteries/Data/Rat/Basic.lean
+++ b/Batteries/Data/Rat/Basic.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Batteries.Data.Nat.Gcd
 import Batteries.Data.Int.DivMod
+import Batteries.Lean.Float
 
 /-! # Basics for the Rational Numbers -/
 
@@ -276,3 +277,19 @@ protected def ceil (a : Rat) : Int :=
     a.num
   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⟩
diff --git a/Batteries/Lean/Float.lean b/Batteries/Lean/Float.lean
index f6d545ec2c..f0b0948e48 100644
--- a/Batteries/Lean/Float.lean
+++ b/Batteries/Lean/Float.lean
@@ -6,6 +6,19 @@
 
 namespace Float
 
+/--
+The floating point value "positive infinity", also used to represent numerical computations
+which produce finite values outside of the representable range of `Float`.
+-/
+def inf : Float := 1/0
+
+/--
+The floating point value "not a number", used to represent erroneous numerical computations
+such as `0 / 0`. Using `nan` in any float operation will return `nan`, and all comparisons
+involving `nan` return `false`, including in particular `nan == nan`.
+-/
+def nan : Float := 0/0
+
 /-- Returns `v, exp` integers such that `f = v * 2^exp`.
 (`e` is not minimal, but `v.abs` will be at most `2^53 - 1`.)
 Returns `none` when `f` is not finite (i.e. `inf`, `-inf` or a `nan`). -/
@@ -58,3 +71,32 @@ def toStringFull (f : Float) : String :=
         s!"{intPart}.{rem.extract ⟨1⟩ rem.endPos}"
     if v < 0 then s!"-{s}" else s
   else f.toString -- inf, -inf, nan
+
+end Float
+
+/--
+Divide two natural numbers, to produce a correctly rounded (nearest-ties-to-even) `Float` result.
+-/
+protected def Nat.divFloat (a b : Nat) : Float :=
+  if b = 0 then
+    if a = 0 then Float.nan else Float.inf
+  else
+    let ea := a.log2
+    let eb := b.log2
+    if eb + 1024 < ea then Float.inf else
+    let eb' := if b <<< ea ≤ a <<< eb then eb else eb + 1
+    let mantissa : UInt64 := (a <<< (eb' + 53) / b <<< ea).toUInt64
+    let rounded := if mantissa &&& 3 == 1 && a <<< (eb' + 53) == mantissa.toNat * (b <<< ea) then
+      mantissa >>> 1
+    else
+      (mantissa + 1) >>> 1
+    rounded.toFloat.scaleB (ea - (eb' + 52))
+
+/--
+Divide two integers, to produce a correctly rounded (nearest-ties-to-even) `Float` result.
+-/
+protected def Int.divFloat (a b : Int) : Float :=
+  if (a ≥ 0) == (b ≥ 0) then
+    a.natAbs.divFloat b.natAbs
+  else
+    -a.natAbs.divFloat b.natAbs
diff --git a/test/float.lean b/test/float.lean
index 204a4b5d43..7d8e7363e1 100644
--- a/test/float.lean
+++ b/test/float.lean
@@ -41,3 +41,28 @@ import Batteries.Lean.Float
 #guard 1e1000.toStringFull == "inf"
 #guard (-1e1000).toStringFull == "-inf"
 #guard (-0/0:Float).toStringFull == "NaN"
+
+#guard Nat.divFloat 1 0 == Float.inf
+#guard Nat.divFloat 50 0 == Float.inf
+#guard (Nat.divFloat 0 0).isNaN
+#guard Nat.divFloat 1 3 == (1 / 3 : Float)
+#guard Nat.divFloat 1 6 == (1 / 6 : Float)
+#guard Nat.divFloat 2 3 == (2 / 3 : Float)
+#guard Nat.divFloat 100 17 == (100 / 17 : Float)
+#guard Nat.divFloat 5000000000000000 1 == (5000000000000000 : Float)
+#guard [0,0,0,1,1,1,2,2,2,2,2,3,3,3,4,4,4].enum.all fun p =>
+  Nat.divFloat (5000000000000000*4+p.1) 4 == (5000000000000000+p.2).toFloat
+#guard Nat.divFloat ((2^53-1)*(2^(1024-53))) 1 == ((2^53-1)*(2^(1024-53)))
+#guard Nat.divFloat (((2^53-1)*4+1)*(2^(1024-53))) 4 == ((2^53-1)*(2^(1024-53)))
+#guard Nat.divFloat (((2^53-1)*4+2)*(2^(1024-53))) 4 == Float.inf
+#guard Nat.divFloat (((2^53-1)*4+3)*(2^(1024-53))) 4 == Float.inf
+#guard Nat.divFloat (((2^53-1)*4+4)*(2^(1024-53))) 4 == Float.inf
+
+#guard Int.divFloat 1 3 == (1 / 3 : Float)
+#guard Int.divFloat (-1) 3 == (-1 / 3 : Float)
+#guard Int.divFloat 1 (-3) == (1 / -3 : Float)
+#guard Int.divFloat (-1) (-3) == (-1 / -3 : Float)
+#guard Int.divFloat (-1) 0 == -Float.inf
+#guard (Int.divFloat 0 0).isNaN
+#guard (Int.divFloat 0 1).toString == "0.000000"
+#guard (Int.divFloat 0 (-1)).toString == "-0.000000"