Theorems · Theorem · group theory

Multiset.noncommSum_add

∀ {α : Type u_3} [inst : AddMonoid α] (s t : Multiset α) (comm : {x | x ∈ s + t}.Pairwise AddCommute),
  (s + t).noncommSum comm = s.noncommSum ⋯ + t.noncommSum ⋯

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddMonoid