Theorems · Theorem · group theory

Finset.map_noncommSum

∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddMonoid β] [inst_1 : AddMonoid γ]
  [inst_2 : FunLike F β γ] [inst_3 : AddMonoidHomClass F β γ] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (g : F),
  g (s.noncommSum f comm) = s.noncommSum (fun i => g (f i)) ⋯

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddMonoidAddMonoidFunLikeAddMonoidHomClass