Theorems · Theorem · group theory

Finset.map_noncommProd

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

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

5 results in Mathlib

Foundations

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

Assumes

MonoidMonoidFunLikeMonoidHomClass