mathlib3 documentation

data.nat.sqrt

Square root of natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines an efficient binary implementation of the square root function that returns the unique r such that r * r ≤ n < (r + 1) * (r + 1). It takes advantage of the binary representation by replacing the multiplication by 2 appearing in (a + b)^2 = a^2 + 2 * a * b + b^2 by a bitmask manipulation.

Reference #

See [Wikipedia, Methods of computing square roots] (https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)).

theorem nat.sqrt_aux_dec {b : } (h : b 0) :
b.shiftr 2 < b

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.sqrt_le' (n : ) :
nat.sqrt n ^ 2 n
theorem nat.lt_succ_sqrt (n : ) :
theorem nat.lt_succ_sqrt' (n : ) :
n < (nat.sqrt n).succ ^ 2
theorem nat.le_sqrt {m n : } :
m nat.sqrt n m * m n
theorem nat.le_sqrt' {m n : } :
m nat.sqrt n m ^ 2 n
theorem nat.sqrt_lt {m n : } :
nat.sqrt m < n m < n * n
theorem nat.sqrt_lt' {m n : } :
nat.sqrt m < n m < n ^ 2
theorem nat.sqrt_le_self (n : ) :
theorem nat.sqrt_le_sqrt {m n : } (h : m n) :
@[simp]
theorem nat.sqrt_zero  :
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.eq_sqrt' {n q : } :
q = nat.sqrt n q ^ 2 n n < (q + 1) ^ 2
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_add_eq' (n : ) {a : } (h : a n + n) :
nat.sqrt (n ^ 2 + a) = n
theorem nat.sqrt_eq (n : ) :
nat.sqrt (n * n) = n
theorem nat.sqrt_eq' (n : ) :
nat.sqrt (n ^ 2) = n
@[simp]
theorem nat.sqrt_one  :
theorem nat.exists_mul_self (x : ) :
( (n : ), n * n = x) nat.sqrt x * nat.sqrt x = x
theorem nat.exists_mul_self' (x : ) :
( (n : ), n ^ 2 = x) nat.sqrt x ^ 2 = x
theorem nat.sqrt_mul_sqrt_lt_succ' (n : ) :
nat.sqrt n ^ 2 < n + 1
theorem nat.succ_le_succ_sqrt (n : ) :
n + 1 (nat.sqrt n + 1) * (nat.sqrt n + 1)
theorem nat.succ_le_succ_sqrt' (n : ) :
n + 1 (nat.sqrt n + 1) ^ 2
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)²

theorem nat.not_exists_sq' {n m : } (hl : m ^ 2 < n) (hr : n < (m + 1) ^ 2) :
¬ (t : ), t ^ 2 = n