English
For r, r' in the graded direct sum, the nth coefficient of their product is the sum over all pairs (i, j) with i + j = n of the products of their coefficients. This can be written as a summation over the full dfinsupp representations.
Русский
У произведения двух элементов градуированного прямого суммирования коэффициент при n равен сумме по всем парам (i, j) с i + j = n от произведений их коэффициентов.
LaTeX
$$$$(r * r')_n = \sum_{i \in \operatorname{supp}(r)} \sum_{j \in \operatorname{supp}(r')} [i+j=n]\; r_i \; r'_j.$$$$
Lean4
theorem coe_mul_apply_eq_dfinsuppSum [AddMonoid ι] [SetLike.GradedMonoid A] [∀ (i : ι) (x : A i), Decidable (x ≠ 0)]
(r r' : ⨁ i, A i) (n : ι) :
((r * r') n : R) = r.sum fun i ri => r'.sum fun j rj => if i + j = n then (ri * rj : R) else 0 :=
by
rw [mul_eq_dfinsuppSum]
iterate 2 rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finset_sum]; congr; ext
dsimp only
split_ifs with h
· subst h
rw [of_eq_same]
rfl
· rw [of_eq_of_ne _ _ _ (Ne.symm h)]
rfl
