inner_eq_one_iff_of_norm_one — Mathlib

English

In the complex field, the inner product satisfies ⟪x,y⟫ = conj(x) · y.

Русский

В комплексном поле выполняется ⟪x,y⟫ = conj(x) · y.

LaTeX

$$$\langle x,y\rangle = \overline{x} \cdot y$$$

Lean4

/-- If the inner product of two unit vectors is `1`, then the two vectors are equal. One form of
the equality case for Cauchy-Schwarz. -/
theorem inner_eq_one_iff_of_norm_one {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ⟪x, y⟫ = 1 ↔ x = y := by
  convert inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E) using 2 <;> simp [hx, hy]

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