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.

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
    @[implicit_reducible]
    instance Rat.instDecidablePredIsSquare :
    DecidablePred IsSquare

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

    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))