Square root on rational numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

rat.sqrt q = rat.mk (int.sqrt q.num) ↑(nat.sqrt q.denom)

source

theorem rat.sqrt_eq (q : ℚ) :

rat.sqrt (q * q) = |q|

source

theorem rat.exists_mul_self (x : ℚ) :

(∃ (q : ℚ), q * q = x) ↔ rat.sqrt x * rat.sqrt x = x

source

theorem rat.sqrt_nonneg (q : ℚ) :

0 ≤ rat.sqrt q