div_sqrt

Mathlib.Data.Real.Sqrt

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

English

For all x ∈ ℝ, x/√x = √x.

Русский

Для любого x ∈ ℝ верно x/√x = √x.

LaTeX

$$$\\\\forall x \\\\in \\\\mathbb{R}, \\\\frac{x}{\\\\sqrt{x}} = \\\\sqrt{x}$$$

Lean4

@[simp]
theorem div_sqrt : x / √x = √x := by grind

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

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

Разделы

Аффилиация

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