Theorems · Theorem · combinatorics

Sym.count_coe_fill_of_ne

∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] {a x : α} {i : Fin (n + 1)} {s : Sym α (n - ↑i)},
  x ≠ a → Multiset.count x ↑(Sym.fill a i s) = Multiset.count x ↑s

Defined in

Mathlib.Data.Sym.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEq