Theorems · Definition · group theory

Multiset.noncommProd

{α : Type u_3} → [inst : Monoid α] → (s : Multiset α) → {x | x ∈ s}.Pairwise Commute → α

Product of a s : Multiset α with [Monoid α], given a proof that * commutes on all elements x ∈ s.

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

23 results in Mathlib

Foundations

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

Assumes

Monoid