sqrt_mul'

Mathlib.Data.Real.Sqrt

URI: https://scilib.ai/kg/mathlib#Real.sqrt_mul'

English

For x ≥ 0 and y ≥ 0, √(x y) = √x · √y.

Русский

Для x ≥ 0 и y ≥ 0 выполняется √(xy) = √x · √y.

LaTeX

$$$x \ge 0 \Rightarrow \forall y \ge 0, \sqrt{xy} = \sqrt{x}\sqrt{y}$$$

Lean4

@[simp]
theorem sqrt_mul' (x) {y : ℝ} (hy : 0 ≤ y) : √(x * y) = √x * √y := by rw [mul_comm, sqrt_mul hy, mul_comm]

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

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

Разделы

Аффилиация

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