Theorems · Theorem · group theory

Finset.sum_fn

∀ {α : Type u_7} {M : α → Type u_8} {ι : Type u_9} [inst : (a : α) → AddCommMonoid (M a)] (s : Finset ι)
  (g : ι → (a : α) → M a), ∑ c ∈ s, g c = fun a => ∑ c ∈ s, g c a

An 'unapplied' analogue of Finset.sum_apply.

Defined in

Mathlib.Algebra.BigOperators.Pi

Cited by

21 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

AddCommMonoid