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.

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