English
Let R and S be additive commutative monoids and let (β_i) be a family of such structures indexed by i in ι. If h: R →+ S is an additive monoid homomorphism, f = (f_i) with finite support (f_i ∈ β_i), and g_i: β_i →+ R are additive homomorphisms, then h distributes over the dependent finite-support sum: h(sumAddHom g f) = sumAddHom (i ↦ h ∘ g_i) f.
Русский
Пусть R и S — аддитивные коммутативные полугруппы, а (β_i) — семейство таких структур, индексированное i из ι. Пусть h: R →+ S — гомоморфизм аддитивных классов, f = (f_i) с конечной опорой (f_i ∈ β_i), и для каждого i задано g_i: β_i →+ R. Тогда сумма по DFinsupp сочетается с отображением: h(sumAddHom g f) = sumAddHom (i ↦ h ∘ g_i) f.
LaTeX
$$$ h\bigl(\mathrm{sumAddHom}\, g\, f\bigr) = \mathrm{sumAddHom}\bigl(\lambda i. h \circ (g i)\bigr) f $$$
Lean4
@[simp]
theorem map_dfinsuppSumAddHom [AddCommMonoid R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)] (h : R →+ S) (f : Π₀ i, β i)
(g : ∀ i, β i →+ R) : h (sumAddHom g f) = sumAddHom (fun i => h.comp (g i)) f :=
DFunLike.congr_fun (comp_liftAddHom h g) f
