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.

Instances For
    source
    theorem Rat.sqrt_eq (q : ℚ) :
    sqrt (q * q) = |q|
    source
    theorem Rat.exists_mul_self (x : ℚ) :
    (∃ (q : ℚ), q * q = x) ↔ sqrt x * sqrt x = x
    source
    theorem Rat.sqrt_nonneg (q : ℚ) :
    0 ≤ sqrt q
    source
    @[implicit_reducible]
    instance Rat.instDecidablePredIsSquare :
    DecidablePred IsSquare

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

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