real_inner_smul_self_right — Mathlib

English

The real inner product of x with a real scalar multiple r x equals r times the square of the norm of x.

Русский

Действительное скалярное произведение вектора x на скаляр r умноженное на x равно r на квадрат нормы x.

LaTeX

$$$$ \\langle x, r\\cdot x \\rangle_{\\mathbb{R}} = r \\cdot \\|x\\|^2. $$$$

Lean4

/-- The inner product of a vector with a multiple of itself. -/
theorem real_inner_smul_self_right (x : F) (r : ℝ) : ⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖) := by
  rw [inner_smul_right, ← real_inner_self_eq_norm_mul_norm]

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