Theorems · Theorem · group theory

Multiset.noncommFold_cons

∀ {α : Type u_3} (op : α → α → α) [assoc : Std.Associative op] (s : Multiset α) (a : α)
  (h : {x | x ∈ a ::ₘ s}.Pairwise fun x y => op x y = op y x) (h' : {x | x ∈ s}.Pairwise fun x y => op x y = op y x)
  (x : α), Multiset.noncommFold op (a ::ₘ s) h x = op a (Multiset.noncommFold op s h' x)

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.Associative