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 : } (h : b 0) :
b.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 (n : ) :

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' : } (h₂ : r + b + n' = n) :
b.sqrt_aux r n = (b.shiftr 2).sqrt_aux (r.div2 + b) n'
theorem nat.sqrt_aux_2 {r n b : } (h : b 0) (h₂ : n < r + b) :
b.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 : } (h : m 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 : } (h : nat.sqrt n = 1) :
n 3
theorem nat.sqrt_lt_self {n : } (h : 1 < n) :
theorem nat.sqrt_pos {n : } :
0 < nat.sqrt n 0 < n
theorem nat.sqrt_add_eq (n : ) {a : } (h : a n + n) :
nat.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
theorem nat.sqrt_mul_sqrt_lt_succ (n : ) :
(nat.sqrt n) * nat.sqrt n < n + 1
theorem nat.succ_le_succ_sqrt (n : ) :
n + 1 (nat.sqrt n + 1) * (nat.sqrt n + 1)
theorem nat.not_exists_sq {n m : } (hl : m * m < n) (hr : n < (m + 1) * (m + 1)) :
¬∃ (t : ), t * t = n

There are no perfect squares strictly between m² and (m+1)²