Theorems · Theorem · group theory

AddMonoidHom.map_finsum_Prop

∀ {M : Type u_2} {N : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {p : Prop} (f : M →+ N) (g : p → M),
  f (∑ᶠ (x : p), g x) = ∑ᶠ (x : p), f (g x)

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid