English
Square root on rationals is defined by taking the integer square root of the numerator and the square root (on naturals) of the denominator: sqrt(q) = mkRat(Int.sqrt(q.num), Nat.sqrt(q.den)).
Русский
Квадратный корень на поле рациональных чисел задаётся как sqrt(q) = mkRat(Int.sqrt(q.num), Nat.sqrt(q.den)).
LaTeX
$$$ \operatorname{sqrt}(q) = \operatorname{mkRat}(\operatorname{Int.sqrt}(q_{\text{num}}), \operatorname{Nat.sqrt}(q_{\text{den}})) $$$
Lean4
/-- 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. -/
@[pp_nodot]
def sqrt (q : ℚ) : ℚ :=
mkRat (Int.sqrt q.num) (Nat.sqrt q.den)
