English
Let x,y ∈ F with x,y ≠ 0. Then ⟪x,y⟫ℝ = ∥x∥ · ∥y∥ if and only if y is a nonnegative real multiple of x, i.e. y = (∥y∥/∥x∥) x with a nonnegative scalar.
Русский
Пусть x,y ∈ F, x≠0,y≠0. Тогда ⟪x,y⟫ℝ = ∥x∥ ∥y∥ тогда и только тогда, когда y = (∥y∥/∥x∥) x с неотрицательным множителем.
LaTeX
$$$⟪x,y⟫_{\mathbb{R}} = ∥x∥ ∥y∥ \iff y = (∥y∥/∥x∥) x\; (\text{ с неотрицательным коэффициентом})$$$
Lean4
/-- If the inner product of two vectors is equal to the product of their norms (i.e.,
`⟪x, y⟫ = ‖x‖ * ‖y‖`), then the two vectors are nonnegative real multiples of each other. One form
of the equality case for Cauchy-Schwarz.
Compare `norm_inner_eq_norm_iff`, which takes the weaker hypothesis `abs ⟪x, y⟫ = ‖x‖ * ‖y‖`. -/
theorem inner_eq_norm_mul_iff_real {x y : F} : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y :=
inner_eq_norm_mul_iff
