HepLean Documentation

Mathlib.Data.Nat.Sqrt

Properties of the natural number square root function. #

sqrt #

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

source
@[irreducible]
theorem Nat.sqrt.iter_sq_le (n guess : ℕ) :
Nat.sqrt.iter n guess * Nat.sqrt.iter n guess ≤ n
source
@[irreducible]
theorem Nat.sqrt.lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) :
n < (Nat.sqrt.iter n guess + 1) * (Nat.sqrt.iter n guess + 1)
source
theorem Nat.sqrt_le (n : ℕ) :
n.sqrt * n.sqrt ≤ n
source
theorem Nat.sqrt_le' (n : ℕ) :
n.sqrt ^ 2 ≤ n
source
theorem Nat.lt_succ_sqrt (n : ℕ) :
n < n.sqrt.succ * n.sqrt.succ
source
theorem Nat.lt_succ_sqrt' (n : ℕ) :
n < n.sqrt.succ ^ 2
source
theorem Nat.sqrt_le_add (n : ℕ) :
n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt
source
theorem Nat.le_sqrt {m n : ℕ} :
m ≤ n.sqrt ↔ m * m ≤ n
source
theorem Nat.le_sqrt' {m n : ℕ} :
m ≤ n.sqrt ↔ m ^ 2 ≤ n
source
theorem Nat.sqrt_lt {m n : ℕ} :
m.sqrt < n ↔ m < n * n
source
theorem Nat.sqrt_lt' {m n : ℕ} :
m.sqrt < n ↔ m < n ^ 2
source
theorem Nat.sqrt_le_self (n : ℕ) :
n.sqrt ≤ n
source
theorem Nat.sqrt_le_sqrt {m n : ℕ} (h : m ≤ n) :
m.sqrt ≤ n.sqrt
source
@[simp]
theorem Nat.sqrt_zero :
Nat.sqrt 0 = 0
source
@[simp]
theorem Nat.sqrt_one :
Nat.sqrt 1 = 1
source
theorem Nat.sqrt_eq_zero {n : ℕ} :
n.sqrt = 0 ↔ n = 0
source
theorem Nat.eq_sqrt {n a : ℕ} :
a = n.sqrt ↔ a * a ≤ n ∧ n < (a + 1) * (a + 1)
source
theorem Nat.eq_sqrt' {n a : ℕ} :
a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2
source
theorem Nat.le_three_of_sqrt_eq_one {n : ℕ} (h : n.sqrt = 1) :
n ≤ 3
source
theorem Nat.sqrt_lt_self {n : ℕ} (h : 1 < n) :
n.sqrt < n
source
theorem Nat.sqrt_pos {n : ℕ} :
0 < n.sqrt ↔ 0 < n
source
theorem Nat.sqrt_add_eq {a : ℕ} (n : ℕ) (h : a ≤ n + n) :
(n * n + a).sqrt = n
source
theorem Nat.sqrt_add_eq' {a : ℕ} (n : ℕ) (h : a ≤ n + n) :
(n ^ 2 + a).sqrt = n
source
theorem Nat.sqrt_eq (n : ℕ) :
(n * n).sqrt = n
source
theorem Nat.sqrt_eq' (n : ℕ) :
(n ^ 2).sqrt = n
source
theorem Nat.sqrt_succ_le_succ_sqrt (n : ℕ) :
n.succ.sqrt ≤ n.sqrt.succ
source
theorem Nat.exists_mul_self (x : ℕ) :
(∃ (n : ℕ), n * n = x) ↔ x.sqrt * x.sqrt = x
source
theorem Nat.exists_mul_self' (x : ℕ) :
(∃ (n : ℕ), n ^ 2 = x) ↔ x.sqrt ^ 2 = x
source
theorem Nat.sqrt_mul_sqrt_lt_succ (n : ℕ) :
n.sqrt * n.sqrt < n + 1
source
theorem Nat.sqrt_mul_sqrt_lt_succ' (n : ℕ) :
n.sqrt ^ 2 < n + 1
source
theorem Nat.succ_le_succ_sqrt (n : ℕ) :
n + 1 ≤ (n.sqrt + 1) * (n.sqrt + 1)
source
theorem Nat.succ_le_succ_sqrt' (n : ℕ) :
n + 1 ≤ (n.sqrt + 1) ^ 2
source
theorem Nat.not_exists_sq {m n : ℕ} (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)²

source
theorem Nat.not_exists_sq' {m n : ℕ} :
m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ (t : ℕ), t ^ 2 = n