sqrt_eq_iff_mul_self_eq_of_pos

Mathlib.Data.Real.Sqrt

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

English

If y > 0, then √x = y is equivalent to x = y^2.

Русский

Пусть y > 0. Тогда √x = y эквивалентно x = y^2.

LaTeX

$$$y > 0 \quad\Rightarrow\quad \sqrt{x} = y \iff x = y^2$$$

Lean4

theorem sqrt_eq_iff_mul_self_eq_of_pos (h : 0 < y) : √x = y ↔ y * y = x := by simp [sqrt_eq_cases, h.ne', h.le]

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

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

Разделы

Аффилиация

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