Documentation

Mathlib.Data.Int.Sqrt

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
    Instances For
      theorem Int.sqrt_eq (n : ) :
      sqrt (n * n) = n.natAbs
      theorem Int.exists_mul_self (x : ) :
      ( (n : ), n * n = x) sqrt x * sqrt x = x
      theorem Int.sqrt_nonneg (n : ) :
      0 sqrt n
      @[simp]
      theorem Int.sqrt_natCast (n : ) :
      sqrt n = n.sqrt
      @[simp]
      theorem Int.sqrt_ofNat (n : ) :