Theorems · Theorem · functional analysis

real_inner_div_norm_mul_norm_eq_neg_one_iff

∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  inner ℝ x y / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

The inner product of two vectors, divided by the product of their norms, has value -1 if and only if they are nonzero and one is a negative multiple of the other.

Defined in

Mathlib.Analysis.InnerProductSpace.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpace