English
Let x,y ∈ E. The equality ⟪x,y⟫ = ‖x‖ · ‖y‖ holds if and only if y is a nonnegative real multiple of x, i.e. y = t x with t ≥ 0.
Русский
Пусть x,y ∈ E. Равенство ⟪x,y⟫ = ‖x‖‖y‖ держится тогда и только тогда, когда y является неотрицательным вещественным кратным x, то есть y = t x с t ≥ 0.
LaTeX
$$$⟪x,y⟫ = ∥x∥ ∥y∥ \iff y = t x \text{ for some } t \ge 0$$$
Lean4
theorem inner_eq_norm_mul_iff_div {x y : E} (h₀ : x ≠ 0) : ⟪x, y⟫ = (‖x‖ : 𝕜) * ‖y‖ ↔ (‖y‖ / ‖x‖ : 𝕜) • x = y :=
by
have h₀' := h₀
rw [← norm_ne_zero_iff, Ne, ← @ofReal_eq_zero 𝕜] at h₀'
constructor <;> intro h
· have : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫ : 𝕜) • x := ((norm_inner_eq_norm_tfae 𝕜 x y).out 0 1).1 (by simp [h])
rw [this.resolve_left h₀, h]
simp [norm_smul, inner_self_ofReal_norm, mul_div_cancel_right₀ _ h₀']
· conv_lhs => rw [← h, inner_smul_right, inner_self_eq_norm_sq_to_K]
field_simp
