inner_eq_norm_sq_left_iff — Mathlib

English

For general 𝕜-valued inner products, ⟪v,w⟫_𝕜 = ‖v‖^2 iff ⟪v, v - w⟫_𝕜 = 0.

Русский

Для обобщённых скалярных произведений ⟪v,w⟫_𝕜 = ‖v‖^2 тогда и только тогда, когда ⟪v, v - w⟫_𝕜 = 0.

LaTeX

$$$\langle v, w \rangle_{\mathbb{K}} = \|v\|^2 \iff \langle v, v - w \rangle_{\mathbb{K}} = 0$$$

Lean4

theorem inner_eq_norm_sq_left_iff {v w : F} : ⟪v, w⟫_ℝ = ‖v‖ ^ 2 ↔ ⟪v, v - w⟫_ℝ = 0 :=
  inner_eq_ofReal_norm_sq_left_iff

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