Theorems · Theorem · group theory

Fintype.sum_equiv

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

Fintype.sum_equiv is a specialization of Finset.sum_bij that automatically fills in most arguments. See Equiv.sum_comp for a version without h.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Defs

Cited by

35 results in Mathlib

Foundations

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

Assumes

FintypeFintypeAddCommMonoid