Documentation

Mathlib.Data.Rat.Sqrt

Square root on rational numbers #

This file defines the square root function on rational numbers Rat.sqrt and proves several theorems about it.

source
🔸 coverage
def Rat.sqrt (q : ℚ) :
ℚ

Square root function on rational numbers, defined by taking the (integer) square root of the numerator and the square root (on natural numbers) of the denominator.

Equations
    Instances For
      source
      📐 coverage
      theorem Rat.sqrt_eq (q : ℚ) :
      sqrt (q * q) = |q|
      source
      📐 coverage
      theorem Rat.exists_mul_self (x : ℚ) :
      (∃ (q : ℚ), q * q = x) ↔ sqrt x * sqrt x = x
      source
      📐 coverage
      theorem Rat.sqrt_nonneg (q : ℚ) :
      0 ≤ sqrt q
      source
      🔸 coverage
      instance Rat.instDecidablePredIsSquare :
      DecidablePred IsSquare

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

      Equations
        source
        📐 coverage
        @[simp]
        theorem Rat.sqrt_intCast (z : ℤ) :
        sqrt ↑z = ↑(Int.sqrt z)
        source
        📐 coverage
        @[simp]
        theorem Rat.sqrt_natCast (n : ℕ) :
        sqrt ↑n = ↑n.sqrt
        source
        📐 coverage
        @[simp]
        theorem Rat.sqrt_ofNat (n : ℕ) :
        sqrt (OfNat.ofNat n) = ↑(Nat.sqrt (OfNat.ofNat n))