English
Let x ∈ ℝ and y ∈ ℝ with y ≥ 0. Then √(x/y) = √x/√y.
Русский
Пусть x ∈ ℝ и y ∈ ℝ, y ≥ 0. Тогда √(x/y) = √x/√y.
LaTeX
$$$\\\\forall x \\\\in \\\\mathbb{R}, \\\\forall y \\\\in \\\\mathbb{R}, y \\\\ge 0 \\\\Rightarrow \\\\sqrt{\\\\frac{x}{y}} = \\\\frac{\\\\sqrt{x}}{\\\\sqrt{y}}$$$
Lean4
@[simp]
theorem sqrt_div' (x) {y : ℝ} (hy : 0 ≤ y) : √(x / y) = √x / √y := by
rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]