English
Let h be an additive equivalence; the mapDFinsuppSumAddHom commutes with h in the sense that applying h to the sumAddHom equals the sumAddHom of the composed maps.
Русский
Пусть h — аддитивное эквивалентное отображение; операция суммирования DFinsupp совместима с h: применение h к sumAddHom эквивалентно sumAddHom после композиции.
LaTeX
$$$ h\bigl(\mathrm{sumAddHom}\, g\, f\bigr) = \mathrm{sumAddHom}\bigl(\lambda i. h.toAddMonoidHom \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.toAddMonoidHom.comp (g i)) f :=
DFunLike.congr_fun (comp_liftAddHom h.toAddMonoidHom g) f
