mul_self_sqrt

Mathlib.Data.Real.Sqrt

URI: https://scilib.ai/kg/mathlib#Real.mul_self_sqrt

English

For x ≥ 0, the product of the square root with itself equals x: (√x)(√x) = x.

Русский

Пусть x ≥ 0. Тогда √x · √x = x.

LaTeX

$$$x \ge 0 \implies \sqrt{x} \cdot \sqrt{x} = x$$$

Lean4

@[simp]
theorem mul_self_sqrt (h : 0 ≤ x) : √x * √x = x := by
  rw [Real.sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]

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

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

Разделы

Аффилиация

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