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

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

    Equations
    @[simp]
    theorem Rat.sqrt_intCast (z : ) :
    Rat.sqrt z = (Int.sqrt z)
    @[simp]
    theorem Rat.sqrt_natCast (n : ) :
    Rat.sqrt n = n.sqrt
    @[simp]