inv_sqrt_two_sub_one

Mathlib.Data.Real.Sqrt

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

English

(√2 − 1)^{-1} = √2 + 1.

Русский

(√2 − 1)^{-1} = √2 + 1.

LaTeX

$$$(\sqrt{2}-1)^{-1} = \sqrt{2}+1$$$

Lean4

theorem inv_sqrt_two_sub_one : (√2 - 1)⁻¹ = √2 + 1 := by grind

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

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

Разделы

Аффилиация

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