English
If h: R →* S is a ring homomorphism and f and g are as above, then h distributes over the sumAddHom in the DFinsupp setting: h (sumAddHom g f) = sumAddHom (i ↦ h.toAddMonoidHom ∘ (g i)) f.
Русский
Если h: R →* S — кольцевой гомоморфизм и f, g действуют как выше, то он распределяется над суммой в DFinsupp: h(sumAddHom g f) = sumAddHom (i ↦ h.toAddMonoidHom ∘ g i) f.
LaTeX
$$$ h\bigl(\mathrm{sumAddHom}\, g\, f\bigr) = \mathrm{sumAddHom}\bigl(\lambda i. h.to\mathrm{AddMonoidHom} \circ (g i)\bigr) f $$$
Lean4
@[simp]
theorem map_dfinsuppSumAddHom [NonAssocSemiring R] [NonAssocSemiring S] [∀ i, AddZeroClass (β i)] (h : R →+* S)
(f : Π₀ i, β i) (g : ∀ i, β i →+ R) : h (sumAddHom g f) = sumAddHom (fun i => h.toAddMonoidHom.comp (g i)) f :=
DFunLike.congr_fun (comp_liftAddHom h.toAddMonoidHom g) f
