sqrt_two_inv_mul_self

Mathlib.Algebra.Star.CHSH

URI: https://scilib.ai/kg/mathlib#TsirelsonInequality.sqrt_two_inv_mul_self

English

The product of the inverses of √2 with itself equals 1/2 in the real numbers.

Русский

Произведение обратных корня из двух с самим собой равно 1/2 в действительных числах.

LaTeX

$$$(\\sqrt{2})^{-1} \\cdot (\\sqrt{2})^{-1} = (2^{-1} : \\mathbb{R}).$$$

Lean4

theorem sqrt_two_inv_mul_self : (√2)⁻¹ * (√2)⁻¹ = (2⁻¹ : ℝ) :=
  by
  rw [← mul_inv]
  simp

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

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

Разделы

Аффилиация

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