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  :

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
theorem rat.sqrt_eq (q : ) :
rat.sqrt (q * q) = abs q

theorem rat.exists_mul_self (x : ) :
(∃ (q : ), q * q = x) (rat.sqrt x) * = x

theorem rat.sqrt_nonneg (q : ) :
0