English
Let x,y ∈ E with x ≠ 0. Then ⟪x,y⟫ = ∥x∥ · ∥y∥ iff y = (∥y∥/∥x∥) x.
Русский
Пусть x ≠ 0. Тогда ⟪x,y⟫ = ∥x∥ ∥y∥ тогда и только тогда, когда y = (∥y∥/∥x∥) x.
LaTeX
$$$⟪x,y⟫ = ∥x∥ ∥y∥ \iff y = \left(\frac{∥y∥}{∥x∥}\right) x$$$
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 {x y : E} : ⟪x, y⟫ = (‖x‖ : 𝕜) * ‖y‖ ↔ (‖y‖ : 𝕜) • x = (‖x‖ : 𝕜) • y :=
by
rcases eq_or_ne x 0 with (rfl | h₀)
· simp
· rw [inner_eq_norm_mul_iff_div h₀, div_eq_inv_mul, mul_smul, inv_smul_eq_iff₀]
rwa [Ne, ofReal_eq_zero, norm_eq_zero]
