Square root of integers

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.

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 (Int.toNat z))

theorem Int.sqrt_eq (n : ℤ) : Int.sqrt (n * n) = ↑(Int.natAbs n)

theorem Int.exists_mul_self (x : ℤ) : (∃ (n : ℤ), n * n = x) ↔ Int.sqrt x * Int.sqrt x = x

theorem Int.sqrt_nonneg (n : ℤ) : 0 ≤ Int.sqrt n

instance Int.instDecidablePredIntIsSquareInstMulInt : DecidablePred IsSquare

IsSquare can be decided on ℤ by checking against the square root.

Equations

• Int.instDecidablePredIntIsSquareInstMulInt m = decidable_of_iff' (Int.sqrt m * Int.sqrt m = m) ⋯