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.

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
  • q.sqrt = mkRat q.num.sqrt q.den.sqrt
Instances For
    theorem Rat.sqrt_eq (q : ) :
    (q * q).sqrt = |q|
    theorem Rat.exists_mul_self (x : ) :
    (∃ (q : ), q * q = x) x.sqrt * x.sqrt = x
    theorem Rat.sqrt_nonneg (q : ) :
    0 q.sqrt

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

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