inner_add_add_self — Mathlib

English

⟪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 : F) : ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ := by
  simp only [inner_add_left, inner_add_right];
  ring
    -- Expand `⟪x - y, x - y⟫`

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