sqrt_div

Mathlib.Data.Real.Sqrt

URI: https://scilib.ai/kg/mathlib#NNReal.sqrt_div

English

For x,y ≥ 0, sqrt(x/y) = sqrt(x)/sqrt(y).

Русский

Пусть x,y ≥ 0. Тогда √(x/y) = √x/√y.

LaTeX

$$$\\forall x,y \\in \\mathbb{R}_{\\ge 0}, \\sqrt{\\frac{x}{y}} = \\frac{\\sqrt{x}}{\\sqrt{y}}$$$

Lean4

theorem sqrt_div (x y : ℝ≥0) : sqrt (x / y) = sqrt x / sqrt y :=
  map_div₀ sqrtHom x y

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru