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 : ) :
Nat.sqrt n ^ 2 n
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_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.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