Theorems · Definition · group theory

Finset.noncommProd

{α : Type u_3} →
  {β : Type u_4} → [inst : Monoid β] → (s : Finset α) → (f : α → β) → (↑s).Pairwise (Function.onFun Commute f) → β

Product of a s : Finset α mapped with f : α → β with [Monoid β], given a proof that * commutes on all elements f x for x ∈ s.

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

44 results in Mathlib

Foundations

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

Assumes

Monoid