English
As above, in the direct sum with dfinsupp, the inner product reduces to the coordinate inner products.
Русский
Как выше, для прямой суммы с использованием dfinsupp скалярное произведение сводится к координатным скалярным произведениям.
LaTeX
$$$\langle V_i v, \sum_j V_j (l_j)\rangle = \langle v, l_i\rangle$$$
Lean4
theorem inner_right_dfinsupp [∀ (i) (x : G i), Decidable (x ≠ 0)] [DecidableEq ι] (l : ⨁ i, G i) (i : ι) (v : G i) :
⟪V i v, l.sum fun j => V j⟫ = ⟪v, l i⟫ :=
calc
⟪V i v, l.sum fun j => V j⟫ = l.sum fun j => fun w => ⟪V i v, V j w⟫ := DFinsupp.inner_sum (fun j => V j) l (V i v)
_ = l.sum fun j => fun w => ite (i = j) ⟪V i v, V j w⟫ 0 :=
(congr_arg l.sum <| funext fun _ => funext <| hV.eq_ite v)
_ = ⟪v, l i⟫ := by
simp only [DFinsupp.sum, Finset.sum_ite_eq, DFinsupp.mem_support_toFun]
split_ifs with h
· simp only [LinearIsometry.inner_map_map]
· simp only [of_not_not h, inner_zero_right]
