mathlib documentation

data.​int.​sqrt

data.​int.​sqrt

def int.​sqrt  :

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
theorem int.​sqrt_eq (n : ) :

theorem int.​exists_mul_self (x : ) :
(∃ (n : ), n * n = x) int.sqrt x * int.sqrt x = x

theorem int.​sqrt_nonneg (n : ) :