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
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
    theorem Rat.sqrt_eq (q : ℚ) :
    Rat.sqrt (q * q) = |q|
    source
    theorem Rat.exists_mul_self (x : ℚ) :
    (∃ (q : ℚ), q * q = x) ↔ Rat.sqrt x * Rat.sqrt x = x
    source
    theorem Rat.sqrt_nonneg (q : ℚ) :
    0 ≤ Rat.sqrt q
    source
    instance Rat.instDecidablePredIsSquare :
    DecidablePred IsSquare

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

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