Theorems · Theorem · group theory

Finset.sum_apply

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

Defined in

Mathlib.Algebra.BigOperators.Pi

Cited by

234 results in Mathlib

Foundations

Depth 16 from the axioms, rests on 150 definitions · uses propext, Quot.sound

Assumes

AddCommMonoid