sqrt_mul_self

Mathlib.Data.Real.Sqrt

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

English

For any NNReal x, sqrt(xx) = x.

Русский

Для любого x ∈ NNReal, sqrt(x·x) = x.

LaTeX

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

Lean4

@[simp]
theorem sqrt_mul_self (x : ℝ≥0) : sqrt (x * x) = x := by rw [← sq, sqrt_sq]

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

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

Разделы

Аффилиация

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