English
Let x,y ∈ E with x ≠ 0,y ≠ 0. Then ⟪x,y⟫ = ∥x∥ ∥y∥ if and only if there exists r ≠ 0 with y = r x.
Русский
Пусть x,y ∈ E, x ≠ 0, y ≠ 0. Тогда ⟪x,y⟫ = ∥x∥ ∥y∥ ⇔ ∃ r ≠ 0: y = r x.
LaTeX
$$$⟪x,y⟫ = ∥x∥ ∥y∥ \iff ∃ r \neq 0 : y = r x$$$
Lean4
/-- 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‖`. -/
theorem norm_inner_eq_norm_iff {x y : E} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ ↔ ∃ r : 𝕜, r ≠ 0 ∧ y = r • x :=
calc
‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ ↔ x = 0 ∨ ∃ r : 𝕜, y = r • x := (norm_inner_eq_norm_tfae 𝕜 x y).out 0 2
_ ↔ ∃ r : 𝕜, y = r • x := (or_iff_right hx₀)
_ ↔ ∃ r : 𝕜, r ≠ 0 ∧ y = r • x :=
⟨fun ⟨r, h⟩ => ⟨r, fun hr₀ => hy₀ <| h.symm ▸ smul_eq_zero.2 <| Or.inl hr₀, h⟩, fun ⟨r, _hr₀, h⟩ => ⟨r, h⟩⟩
