parallelogram_law — Mathlib

English

The parallelogram law holds: ⟪x + y, x + y⟫ + ⟪x - y, x - y⟫ = 2(⟪x,x⟫ + ⟪y,y⟫).

Русский

Свойство параллелограмма: ⟪x + y, x + y⟫ + ⟪x - y, x - y⟫ = 2(⟪x,x⟫ + ⟪y,y⟫).

LaTeX

$$$\langle x + y, x + y \rangle + \langle x - y, x - y \rangle = 2 \big( \langle x, x \rangle + \langle y, y \rangle \big)$$$

Lean4

/-- Parallelogram law -/
theorem parallelogram_law {x y : E} : ⟪x + y, x + y⟫ + ⟪x - y, x - y⟫ = 2 * (⟪x, x⟫ + ⟪y, y⟫) :=
  by
  simp only [inner_add_add_self, inner_sub_sub_self]
  ring

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