Computing a floor involving a square root

Main results

• Nat.sqrt_div_eq_floor_div_sqrt: the floor of a / sqrt b is the natural square root of a² / b, including the zero-denominator convention.

This elementary arithmetic bridge is original adaptation code. It lets finite algorithms use integer arithmetic while retaining their real-valued capacity specifications.

theorem Nat.sqrt_div_eq_floor_div_sqrt (a b : ℕ) : (a ^ 2 / b).sqrt = ⌊↑a / √↑b⌋₊

A computable integer formula for the floor of a quotient by a square root.