Theorems · Theorem · group theory

Finset.sum_comp_equiv

∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : κ → M} (e : ι ≃ κ),
  s.sum (f ∘ ⇑e) = (Finset.map e.toEmbedding s).sum f

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddCommMonoid