abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul

English

If x ≠ 0 and r ≠ 0, then |⟪x, r·x⟫| / (∥x∥ ∥r·x∥) = 1.

Русский

Если x ≠ 0 и r ≠ 0, то |⟪x, r·x⟫| / (∥x∥ ∥r·x∥) = 1.

LaTeX

$$$\left|\langle x, r\cdot x\rangle\right| / (\|x\| \|r\cdot x\|) = 1$$$

Lean4

/-- The inner product of a nonzero vector with a nonzero multiple of
itself, divided by the product of their norms, has absolute value
1. -/
theorem abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r ≠ 0) :
    |⟪x, r • x⟫_ℝ| / (‖x‖ * ‖r • x‖) = 1 :=
  norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr

Похожие утверждения