English
For f : SkewMonoidAlgebra k G and g : G → k → SkewMonoidAlgebra k' G', the toFinsupp of sum equals Finsupp.sum of toFinsupps: (sum f g).toFinsupp = Finsupp.sum f.toFinsupp (toFinsupp ∘ g).
Русский
Для f и g как выше, toFinsupp суммы равен сумме toFinsupp: (sum f g).toFinsupp = Finsupp.sum f.toFinsupp (toFinsupp ∘ g).
LaTeX
$$$ (\\mathrm{sum}\\ f\\ g).\\mathrm{toFinsupp} = \\mathrm{Finsupp}.sum\\ f.toFinsupp (toFinsupp \\circ g) $$$
Lean4
/-- Variant where the image of `g` is a `SkewMonoidAlgebra`. -/
theorem toFinsupp_sum' {k' G' : Type*} [AddCommMonoid k'] (f : SkewMonoidAlgebra k G)
(g : G → k → SkewMonoidAlgebra k' G') : (sum f g).toFinsupp = Finsupp.sum f.toFinsupp (toFinsupp <| g · ·) :=
_root_.map_sum toFinsuppAddEquiv (fun a ↦ g a (f.coeff a)) f.toFinsupp.support
