prod_inner_apply — Mathlib

English

The inner product on the product basis decomposes componentwise: ⟪v.prod w, x.prod y⟫ = ⟪(v.x).fst, (x).fst⟫ + ⟪(v.x).snd, (x).snd⟫ (with appropriate identifications).

Русский

Внутреннее произведение на основе произведения раскладывается по компонентам: ⟪v.prod w, x.prod y⟫ = ⟪v.fst, x.fst⟫ + ⟪v.snd, x.snd⟫.

LaTeX

$$$\langle v \cdot w, x \cdot y \rangle = \langle v_{1}, x_{1} \rangle + \langle w_{2}, y_{2} \rangle$$$

Lean4

@[simp]
theorem prod_inner_apply (x y : WithLp 2 (E × F)) :
    ⟪x, y⟫_𝕜 = ⟪(ofLp x).fst, (ofLp y).fst⟫_𝕜 + ⟪(ofLp x).snd, (ofLp y).snd⟫_𝕜 :=
  rfl

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