norm_add_sq — Mathlib

English

For x ∈ E, 0 < Re ⟪x, x⟫ iff x ≠ 0.

Русский

Для x ∈ E верно: 0 < Re ⟪x, x⟫ тогда и только тогда, когда x ≠ 0.

LaTeX

$$$0 < \operatorname{Re}\langle x, x\rangle \Longleftrightarrow x \neq 0$$$

Lean4

/-- Expand the square -/
theorem norm_add_sq (x y : E) : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫ + ‖y‖ ^ 2 :=
  by
  repeat' rw [sq (M := ℝ), ← @inner_self_eq_norm_mul_norm 𝕜]
  rw [inner_add_add_self, two_mul]
  simp only [add_assoc, add_left_inj, add_right_inj, AddMonoidHom.map_add]
  rw [← inner_conj_symm, conj_re]

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