Square root of integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the square root function on integers. int.sqrt z is the greatest integer r such that r * r ≤ z. If z ≤ 0, then int.sqrt z = 0.

source

def int.sqrt (z : ℤ) :

ℤ

sqrt z is the square root of an integer z. If z is positive, it returns the largest integer r such that r * r ≤ n. If it is negative, it returns 0. For example, sqrt (-1) = 0, sqrt 1 = 1, sqrt 2 = 1

Equations

int.sqrt z = ↑(nat.sqrt z.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