Theorems · Theorem · group theory

Multiset.noncommFoldr_coe

∀ {α : Type u_3} {β : Type u_4} (f : α → β → β) (l : List α)
  (comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)) (b : β),
  Multiset.noncommFoldr f (↑l) comm b = List.foldr f b l

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

3 results in Mathlib

Foundations

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