inner_add_add_self — Mathlib

English

The inner product of a sum with itself expands: ⟪x+y, x+y⟫ = ⟪x,x⟫ + ⟪x,y⟫ + ⟪y,x⟫ + ⟪y,y⟫.

Русский

Скалярное произведение суммы с самой собой раскладывается: ⟪x+y, x+y⟫ = ⟪x,x⟫ + ⟪x,y⟫ + ⟪y,x⟫ + ⟪y,y⟫.

LaTeX

$$$\langle x + y, x + y \rangle = \langle x, x \rangle + \langle x, y \rangle + \langle y, x \rangle + \langle y, y \rangle$$$

Lean4

/-- Expand `⟪x + y, x + y⟫` -/
theorem inner_add_add_self (x y : E) : ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ := by
  simp only [inner_add_left, inner_add_right]; ring

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