real_inner_smul_self_left — Mathlib

English

Let x be a vector and r a real number. Then the real inner product of r·x with x equals r times the squared norm of x: ⟪r·x, x⟫ℝ = r ∥x∥^2.

Русский

Пусть вектор x и вещественное число r. Тогда ⟪r·x, x⟫ℝ = r ∥x∥^2.

LaTeX

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

Lean4

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

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