sqrt_eq_one

Mathlib.Data.Real.Sqrt

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

English

For NNReal x, sqrt x = 1 iff x = 1.

Русский

Для NNReal x верно: sqrt x = 1 ⇔ x = 1.

LaTeX

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

Lean4

@[simp]
theorem sqrt_eq_one : sqrt x = 1 ↔ x = 1 := by simp [sqrt_eq_iff_eq_sq]

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

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

Разделы

Аффилиация

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