Theorems · Theorem · group theory

Equiv.sum_comp

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

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Defs

Cited by

31 results in Mathlib

Foundations

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

Assumes

FintypeFintypeAddCommMonoid