Theorems · Theorem · functional analysis

norm_inner_eq_norm_iff

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, x ≠ 0 → y ≠ 0 → (‖inner 𝕜 x y‖ = ‖x‖ * ‖y‖ ↔ ∃ r, r ≠ 0 ∧ y = r • x)

If the inner product of two vectors is equal to the product of their norms, then the two vectors are multiples of each other. One form of the equality case for Cauchy-Schwarz. Compare inner_eq_norm_mul_iff, which takes the stronger hypothesis ⟪x, y⟫ = ‖x‖ * ‖y‖.

Defined in

Mathlib.Analysis.InnerProductSpace.Basic

Cited by

2 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpace