English
A heavily unfolded expression for multiplication: a * a' equals the sum over pairs in the product of supports, with each term given by DirectSum.of of GradedMonoid.GMul.mul of the coordinates.
Русский
Грубое развёртывание умножения: a * a' равняется сумме по парам в произведении опор, каждая члена равна DirectSum.of от произведения GradedMonoid.GMul.mul координат.
LaTeX
$$$a * a' = \sum_{(i,j)\in \mathrm{DFinsupp.support}(a) \times \mathrm{DFinsupp.support}(a')} DirectSum.of A (i+j) (GMul.mul a_i a'_j)$$$
Lean4
/-- A heavily unfolded version of the definition of multiplication -/
theorem mul_eq_sum_support_ghas_mul [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (a a' : ⨁ i, A i) :
a * a' =
∑ ij ∈ DFinsupp.support a ×ˢ DFinsupp.support a',
DirectSum.of _ _ (GradedMonoid.GMul.mul (a ij.fst) (a' ij.snd)) :=
by simp only [mul_eq_dfinsuppSum, DFinsupp.sum, Finset.sum_product]
