English
The square root of a real number is defined by converting to NNReal and applying its square root; negative inputs yield 0.
Русский
Квадратный корень из действительного числа определяется через перевод в NNReal и применение square root; отрицательные значения дают 0.
LaTeX
$$$\\sqrt{x} := NNReal.sqrt( Real.toNNReal(x) )$ and is defined to be 0 when $x<0$.$$
Lean4
/-- The square root of a real number. This returns 0 for negative inputs.
This has notation `√x`. Note that `√x⁻¹` is parsed as `√(x⁻¹)`. -/
noncomputable def sqrt (x : ℝ) : ℝ :=
NNReal.sqrt
(Real.toNNReal x)
-- TODO: replace this with a typeclass
