inner_eq_star_dotProduct — Mathlib

English

The symmetry of the L2-inner product on the coordinate space reflects the coordinate-wise decomposition, i.e., the inner product equals the sum of coordinate products.

Русский

Симметрия L2-скалярного произведения на пространстве координат выражается через сумму координатных произведений.

LaTeX

$$$\langle x,y\rangle = \sum_i \langle x_i, y_i\rangle$$$

Lean4

theorem inner_eq_star_dotProduct (x y : EuclideanSpace 𝕜 ι) : ⟪x, y⟫ = ofLp y ⬝ᵥ star (ofLp x) :=
  rfl

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