real_inner_add_add_self — Mathlib

English

For x,y ∈ F (real inner product space), ⟪x+y, x+y⟫_ℝ = ⟪x,x⟫_ℝ + 2⟪x,y⟫_ℝ + ⟪y,y⟫_ℝ.

Русский

Для вещественного пространства: ⟪x+y, x+y⟫_ℝ = ⟪x,x⟫_ℝ + 2⟪x,y⟫_ℝ + ⟪y,y⟫_ℝ.

LaTeX

$$$\langle x+y, x+y \rangle_\mathbb{R} = \langle x,x \rangle_\mathbb{R} + 2 \langle x,y \rangle_\mathbb{R} + \langle y,y \rangle_\mathbb{R}$$$

Lean4

/-- Expand `⟪x + y, x + y⟫_ℝ` -/
theorem real_inner_add_add_self (x y : F) : ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ :=
  by
  have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [← inner_conj_symm]; rfl
  simp only [inner_add_add_self, this, add_left_inj]
  ring
    -- Expand `⟪x - y, x - y⟫`

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