Mathlib.Data.Int.Sqrt

Module docstring

{"# 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. "}

Int.sqrt definition

(z : ℤ) : ℤ

Full source

/-- `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` -/
@[pp_nodot]
def sqrt (z : ℤ) : ℤ :=
  Nat.sqrt <| Int.toNat z

Integer square root function

Informal description

The function `Int.sqrt` computes the integer square root of an integer `z`. For non-negative `z`, it returns the largest integer `r` such that `r * r ≤ z`. For negative `z`, it returns `0`. For example, `Int.sqrt (-1) = 0`, `Int.sqrt 1 = 1`, and `Int.sqrt 2 = 1`.

Int.sqrt_eq theorem

(n : ℤ) : sqrt (n * n) = n.natAbs

Full source

theorem sqrt_eq (n : ℤ) : sqrt (n * n) = n.natAbs := by
  rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq]

Square Root of Square Equals Absolute Value

Informal description

For any integer $n$, the integer square root of $n^2$ is equal to the absolute value of $n$ as a natural number, i.e., $\operatorname{sqrt}(n \cdot n) = |n|_{\mathbb{N}}$.

Int.exists_mul_self theorem

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

Full source

theorem exists_mul_self (x : ℤ) : (∃ n, n * n = x) ↔ sqrt x * sqrt x = x :=
  ⟨fun ⟨n, hn⟩ => by rw [← hn, sqrt_eq, ← Int.natCast_mul, natAbs_mul_self], fun h => ⟨sqrt x, h⟩⟩

Existence of Square Root in Integers is Equivalent to Perfect Square Condition

Informal description

For any integer $x$, there exists an integer $n$ such that $n^2 = x$ if and only if the square of the integer square root of $x$ equals $x$, i.e., $(\exists n \in \mathbb{Z}, n^2 = x) \leftrightarrow (\operatorname{sqrt}(x))^2 = x$.

Int.sqrt_nonneg theorem

(n : ℤ) : 0 ≤ sqrt n

Full source

theorem sqrt_nonneg (n : ℤ) : 0 ≤ sqrt n :=
  natCast_nonneg _

Non-negativity of Integer Square Root

Informal description

For any integer $n$, the integer square root of $n$ is non-negative, i.e., $0 \leq \operatorname{sqrt}(n)$.

Int.sqrt_natCast theorem

(n : ℕ) : Int.sqrt (n : ℤ) = Nat.sqrt n

Full source

@[simp, norm_cast]
theorem sqrt_natCast (n : ℕ) : Int.sqrt (n : ℤ) = Nat.sqrt n := by rw [sqrt, toNat_natCast]

Integer Square Root of Natural Number Cast Equals Natural Square Root

Informal description

For any natural number $n$, the integer square root of $n$ (viewed as an integer) is equal to the natural number square root of $n$, i.e., $\text{Int.sqrt}(n) = \text{Nat.sqrt}(n)$.

Int.sqrt_ofNat theorem

(n : ℕ) : Int.sqrt ofNat(n) = Nat.sqrt ofNat(n)

Full source

@[simp]
theorem sqrt_ofNat (n : ℕ) : Int.sqrt ofNat(n) = Nat.sqrt ofNat(n) :=
  sqrt_natCast _

Integer Square Root of Natural Number Equals Natural Square Root

Informal description

For any natural number $n$, the integer square root of $n$ (viewed as an integer via the canonical embedding) is equal to the natural number square root of $n$, i.e., $\operatorname{Int.sqrt}(n) = \operatorname{Nat.sqrt}(n)$.