dotProduct_block — Mathlib

English

The dot product on a direct sum splits into the sum of dot products on the two summands: v ⬝ᵥ w = v ∘ Sum.inl ⬝ᵥ w ∘ Sum.inl + v ∘ Sum.inr ⬝ᵥ w ∘ Sum.inr.

Русский

Скалярное произведение на прямом сумме раскладывается на сумму по двум компонентам: v ⬝ w = v ∘ inl ⬝ w ∘ inl + v ∘ inr ⬝ w ∘ inr.

LaTeX

$$$v \;\Diamond\; w = v \circ \mathrm{Sum.inl} \;\diamond\; w \circ \mathrm{Sum.inl} + v \circ \mathrm{Sum.inr} \;\diamond\; w \circ \mathrm{Sum.inr}$$$

Lean4

theorem dotProduct_block [Fintype m] [Fintype n] [Mul α] [AddCommMonoid α] (v w : m ⊕ n → α) :
    v ⬝ᵥ w = v ∘ Sum.inl ⬝ᵥ w ∘ Sum.inl + v ∘ Sum.inr ⬝ᵥ w ∘ Sum.inr :=
  Fintype.sum_sum_type _

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