English
For r in A_i and r' in the sum, the auxiliary coefficient equals the product r · r' at a shifted index when the shift matches the chosen j; this is a technical lemma used to decompose coefficients.
Русский
Для r в A_i и r' в сумме вспомогательный коэффициент равен произведению r и r' на смещённом индексе при совпадении смещения с выбранным j.
LaTeX
$$$$(\text{coeff}) = r \cdot r'_j.$$$$
Lean4
theorem coe_of_mul_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r : A i) (r' : ⨁ i, A i) {j n : ι}
(H : ∀ x : ι, i + x = n ↔ x = j) : ((of (fun i => A i) i r * r') n : R) = r * r' j := by
classical
rw [coe_mul_apply_eq_dfinsuppSum]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, zero_mul, 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, mul_zero]
