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

• Rat.sqrt q = mkRat (Int.sqrt q.num) q.den.sqrt

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

theorem Rat.sqrt_nonneg (q : ℚ) : 0 ≤ Rat.sqrt q

instance Rat.instDecidablePredIsSquare : DecidablePred IsSquare

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

Equations

• m.instDecidablePredIsSquare = decidable_of_iff' (Rat.sqrt m * Rat.sqrt m = m) ⋯

@[simp]

theorem Rat.sqrt_intCast (z : ℤ) : Rat.sqrt ↑z = ↑(Int.sqrt z)

@[simp]

theorem Rat.sqrt_natCast (n : ℕ) : Rat.sqrt ↑n = ↑n.sqrt

@[simp]

theorem Rat.sqrt_ofNat (n : ℕ) : Rat.sqrt (OfNat.ofNat n) = ↑(Nat.sqrt (OfNat.ofNat n))