map_finsuppProd — Mathlib

English

Under a suitable homomorphism h, h(f.prod g) = f.prod (λ a b, h(g a b)).

Русский

При подходящем однородном отображении h выполняется: h(f.prod g) = f.prod (λ a b, h(g a b)).

LaTeX

$$$$ h\\big(f.prod g\\big) = f.prod \\big(\\lambda a b, h\\big(g a b\\big)\\big) $$$$

Lean4

@[to_additive]
theorem map_finsuppProd [Zero M] [CommMonoid N] [CommMonoid P] {H : Type*} [FunLike H N P] [MonoidHomClass H N P]
    (h : H) (f : α →₀ M) (g : α → M → N) : h (f.prod g) = f.prod fun a b => h (g a b) :=
  map_prod h _ _

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