real_inner_smul_left — Mathlib

English

The real inner product is bilinear in the left argument: ⟪r x, y⟫ = r ⟪x, y⟫ for r ∈ ℝ.

Русский

Действительно, вещественное скалярное произведение линейно по левому аргументу: ⟪r x, y⟫ = r ⟪x, y⟫ для r ∈ ℝ.

LaTeX

$$$\langle r x, y\rangle = r \langle x, y\rangle$$$

Lean4

theorem real_inner_smul_left (x y : F) (r : ℝ) : ⟪r • x, y⟫_ℝ = r * ⟪x, y⟫_ℝ :=
  inner_smul_left _ _ _

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