Theorems · Theorem · group theory

Function.Bijective.sum_comp

∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  {e : ι → κ}, Function.Bijective e → ∀ (g : κ → M), ∑ i, g (e i) = ∑ i, g i

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Defs

Cited by

8 results in Mathlib

Foundations

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

Assumes

FintypeFintypeAddCommMonoid