Theorems · Theorem · group theory

AddMonoidHom.map_finsum_plift

∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : M →+ N)
  (g : α → M), Function.HasFiniteSupport (g ∘ PLift.down) → f (∑ᶠ (x : α), g x) = ∑ᶠ (x : α), f (g x)

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

3 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidAddCommMonoid