# Documentation

Mathlib.Data.Nat.Sqrt

# Square root of natural numbers #

This file defines an efficient implementation of the square root function that returns the unique r such that r * r ≤ n < (r + 1) * (r + 1).

## 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_le (n : ) :
n
theorem Nat.sqrt_le' (n : ) :
^ 2 n
theorem Nat.lt_succ_sqrt' (n : ) :
n < Nat.succ () ^ 2
theorem Nat.sqrt_le_add (n : ) :
n + +
theorem Nat.le_sqrt {m : } {n : } :
m m * m n
theorem Nat.le_sqrt' {m : } {n : } :
m m ^ 2 n
theorem Nat.sqrt_lt {m : } {n : } :
< n m < n * n
theorem Nat.sqrt_lt' {m : } {n : } :
< n m < n ^ 2
theorem Nat.sqrt_le_self (n : ) :
n
theorem Nat.sqrt_le_sqrt {m : } {n : } (h : m n) :
@[simp]
theorem Nat.sqrt_zero :
= 0
theorem Nat.sqrt_eq_zero {n : } :
= 0 n = 0
theorem Nat.eq_sqrt {n : } {q : } :
q = q * q n n < (q + 1) * (q + 1)
theorem Nat.eq_sqrt' {n : } {q : } :
q = q ^ 2 n n < (q + 1) ^ 2
theorem Nat.le_three_of_sqrt_eq_one {n : } (h : = 1) :
n 3
theorem Nat.sqrt_lt_self {n : } (h : 1 < n) :
< n
theorem Nat.sqrt_pos {n : } :
0 < 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 :
= 1
theorem Nat.exists_mul_self (x : ) :
(n, n * n = x) = x
theorem Nat.exists_mul_self' (x : ) :
(n, n ^ 2 = x) ^ 2 = x
theorem Nat.sqrt_mul_sqrt_lt_succ' (n : ) :
^ 2 < n + 1
theorem Nat.succ_le_succ_sqrt (n : ) :
n + 1 ( + 1) * ( + 1)
theorem Nat.succ_le_succ_sqrt' (n : ) :
n + 1 ( + 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