Theorems · Theorem · group theory

Multiset.noncommFold_eq_fold

∀ {α : Type u_3} (op : α → α → α) [assoc : Std.Associative op] (s : Multiset α) [inst : Std.Commutative op] (a : α),
  Multiset.noncommFold op s ⋯ a = Multiset.fold op a s

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

0 results in Mathlib

Foundations

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

Assumes

Std.AssociativeStd.Commutative