sqrt_mul

Mathlib.Data.Real.Sqrt

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

English

The geometric mean property: sqrt(xy) = sqrt x sqrt y for NNReal x,y.

Русский

Свойство геометрического среднего: sqrt(xy) = sqrt x sqrt y для x,y ∈ ℝ≥0.

LaTeX

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

Lean4

theorem sqrt_mul (x y : ℝ≥0) : sqrt (x * y) = sqrt x * sqrt y := by rw [sqrt_eq_iff_eq_sq, mul_pow, sq_sqrt, sq_sqrt]

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

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

Разделы

Аффилиация

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