English
Let r be a direct sum with components r(i) and r' at index i, and suppose H identifies exactly which index j satisfies j+i=n for a fixed n. Then the n-th coefficient of the product r * of i r' is r(j) · r'.
Русский
Пусть r — элемент прямой суммы с компонентами r(i) и r' на индексе i, и предположим, что существует точное соответствие индекса j, удовлетворяющее j+i=n. Тогда n-я координата произведения r на (of i r') равна r(j)·r'.
LaTeX
$$$ (r * of (fun i => A_i) i r')_n = r_j \cdot r' \quad \text{при } \forall x, x+i=n \iff x=j. $$$
Lean4
theorem coe_mul_of_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] (r : ⨁ i, A i) {i : ι} (r' : A i) {j n : ι}
(H : ∀ x : ι, x + i = n ↔ x = j) : ((r * of (fun i => A i) i r') n : R) = r j * r' := by
classical
rw [coe_mul_apply_eq_dfinsuppSum, DFinsupp.sum_comm]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
exact DFinsupp.sum_zero
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
split_ifs with h
· rfl
rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
