Theorems · Theorem · group theory

Finset.sum_fiberwise_of_maps_to

∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ}
  [inst_1 : DecidableEq κ] {g : ι → κ},
  (∀ i ∈ s, g i ∈ t) → ∀ (f : ι → M), ∑ j ∈ t, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s, f i

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Cited by

12 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidableEq