mathlib docs: data.int.sqrt

def int.sqrt (n : ℤ) :

sqrt n is the square root of an integer n. If n is not a perfect square, and is positive, it returns the largest k:ℤ such that k*k ≤ n. If it is negative, it returns 0. For example, sqrt 2 = 1 and sqrt 1 = 1 and sqrt (-1) = 0

Equations

int.sqrt n = ↑(nat.sqrt n.to_nat)

source

theorem int.sqrt_eq (n : ℤ) :

int.sqrt (n * n) = ↑(n.nat_abs)

source

theorem int.exists_mul_self (x : ℤ) :

(∃ (n : ℤ), n * n = x) ↔ (int.sqrt x) * int.sqrt x = x

source

theorem int.sqrt_nonneg (n : ℤ) :

0 ≤ int.sqrt n