mathlib documentation

data.nat.sqrt

Square root of natural numbers

An efficient binary implementation of a (sqrt n) function that returns s such that

s*s  n  s*s + s + s
theorem nat.sqrt_aux_dec {b : } :
b 0b.shiftr 2 < b

def nat.sqrt_aux  :

Auxiliary function for nat.sqrt. See e.g. https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)

Equations
def nat.sqrt  :

sqrt n is the square root of a natural number n. If n is not a perfect square, it returns the largest k:ℕ such that k*k ≤ n.

Equations
theorem nat.sqrt_aux_0 (r n : ) :
0.sqrt_aux r n = r

theorem nat.sqrt_aux_1 {r n b : } (h : b 0) {n' : } :
r + b + n' = nb.sqrt_aux r n = (b.shiftr 2).sqrt_aux (r.div2 + b) n'

theorem nat.sqrt_aux_2 {r n b : } :
b 0n < r + bb.sqrt_aux r n = (b.shiftr 2).sqrt_aux r.div2 n

theorem nat.sqrt_le (n : ) :

theorem nat.lt_succ_sqrt (n : ) :

theorem nat.le_sqrt {m n : } :
m nat.sqrt n m * m n

theorem nat.sqrt_lt {m n : } :
nat.sqrt m < n m < n * n

theorem nat.sqrt_le_self (n : ) :

theorem nat.sqrt_le_sqrt {m n : } :
m nnat.sqrt m nat.sqrt n

theorem nat.sqrt_eq_zero {n : } :
nat.sqrt n = 0 n = 0

theorem nat.eq_sqrt {n q : } :
q = nat.sqrt n q * q n n < (q + 1) * (q + 1)

theorem nat.le_three_of_sqrt_eq_one {n : } :
nat.sqrt n = 1n 3

theorem nat.sqrt_lt_self {n : } :
1 < nnat.sqrt n < n

theorem nat.sqrt_pos {n : } :
0 < nat.sqrt n 0 < n

theorem nat.sqrt_add_eq (n : ) {a : } :
a n + nnat.sqrt (n * n + a) = n

theorem nat.sqrt_eq (n : ) :
nat.sqrt (n * n) = n

theorem nat.exists_mul_self (x : ) :
(∃ (n : ), n * n = x) (nat.sqrt x) * nat.sqrt x = x