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 _