English
Let A be a grading by ι and let r, r' be elements of the graded direct sum ⨁i A_i with finite support. Then the nth component of the product r · r' is the finite sum of all products of components whose indices add to n; i.e. (r · r')_n = ∑_{i+j=n} r_i · r'_j.
Русский
Пусть A задаёт градацию по ι, и пусть r, r' принадлежат к частично-грандиенному прямому суммированию ⨁i A_i с конечной поддержкой. Тогда n-ый компонент произведения r · r' является конечной суммой всех произведений компонент, чьи индексы суммируются в n; тождество (r · r')_n = ∑_{i+j=n} r_i · r'_j.
LaTeX
$$$$(r * r')_n = \\sum_{i,j:\\; i+j=n} (r_i)(r'_j).$$$$
Lean4
theorem coe_mul_apply [AddMonoid ι] [SetLike.GradedMonoid A] [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (r r' : ⨁ i, A i)
(n : ι) : ((r * r') n : R) = ∑ ij ∈ r.support ×ˢ r'.support with ij.1 + ij.2 = n, (r ij.1 * r' ij.2 : R) :=
by
rw [mul_eq_sum_support_ghas_mul, DFinsupp.finset_sum_apply, AddSubmonoidClass.coe_finset_sum]
simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]
