English
Unfolded expression for multiplication as a finite sum over support pairs, using DirectSum.of to inject GradedMonoid.mul of coordinates.
Русский
Развернутое выражение для умножения как конечная сумма по паром опор, через DirectSum.of и произведение координат GradedMonoid.mul.
LaTeX
$$$a * a' = \sum_{ij \in \mathrm{DFinsupp.support}(a) \times \mathrm{DFinsupp.support}(a')} DirectSum.of (\dots) (GMul.mul a_i a'_j)$$$
Lean4
@[simp]
theorem of_zero_pow (a : A 0) : ∀ n : ℕ, of A 0 (a ^ n) = of A 0 a ^ n
| 0 => by
rw [pow_zero, pow_zero, DirectSum.of_zero_one]
-- Porting note: Lean doesn't think this terminates if we only use `of_zero_pow` alone
| n + 1 => by rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ n]
