map_sum — Mathlib

English

For any additive homomorphism h, h (sum f g) = sum f (λ a b, h (g a b)).

Русский

Для любого аддитивного гомоморфизма h выполняется h(∑ f g) = ∑ f (λ a b, h(g a b)).

LaTeX

$$$h\\big(\\mathrm{sum}\\ f\\ g\\big) = \\mathrm{sum}\\ f\\ (\\lambda a\\ b,\\ h(g\\ a\\ b))$$$

Lean4

theorem map_sum {N P : Type*} [AddCommMonoid N] [AddCommMonoid P] {H : Type*} [FunLike H N P] [AddMonoidHomClass H N P]
    (h : H) (f : SkewMonoidAlgebra k G) (g : G → k → N) : h (sum f g) = sum f fun a b ↦ h (g a b) :=
  _root_.map_sum h _ _

Похожие утверждения