Theorems · Theorem · combinatorics

Multiset.countPerms_filter_ne

∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (m : Multiset α),
  m.countPerms = m.card.choose (Multiset.count a m) * (Multiset.filter (fun x => a ≠ x) m).countPerms

Defined in

Mathlib.Data.Nat.Choose.Multinomial

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEq