Theorems · Theorem · group theory

Fintype.sum_bijective

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

Fintype.sum_bijective is a variant of Finset.sum_bij that accepts Function.Bijective. See Function.Bijective.sum_comp for a version without h.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Defs

Cited by

13 results in Mathlib

Foundations

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

Assumes

FintypeFintypeAddCommMonoid