inner_eq_ofReal_norm_sq_right_iff

English

Let E be a complex inner product space over 𝕜. For any v, w ∈ E, ⟨v, w⟩ = ∥w∥^2 if and only if ⟨v − w, w⟩ = 0.

Русский

Пусть E — комплексное скалярно внедренное пространство над 𝕜. Для любых v, w ∈ E верно: ⟨v, w⟩ = ∥w∥^2 тогда и только тогда, когда ⟨v − w, w⟩ = 0.

LaTeX

$$$\langle v, w\rangle = \|w\|^2 \quad\Leftrightarrow\quad \langle v-w, w\rangle = 0$$$

Lean4

theorem inner_eq_ofReal_norm_sq_right_iff {v w : E} : ⟪v, w⟫_𝕜 = ‖w‖ ^ 2 ↔ ⟪v - w, w⟫_𝕜 = 0 := by
  rw [inner_sub_left, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]

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