Theorems · Theorem · combinatorics
Sym.fill_filterNe
∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (a : α) (m : Sym α n),
Sym.fill a (Sym.filterNe a m).fst (Sym.filterNe a m).snd = m- Defined in
- Mathlib.Data.Sym.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- add_zeroproof · cited by 2,707
- Multisetproof · cited by 2,627
- zero_addproof · cited by 2,366
- eq_or_neproof · cited by 1,117
- Multiset.countproof · cited by 302
- Symstatement and proof · cited by 150
- Multiset.filterproof · cited by 102
- Subtype.coe_mkproof · cited by 81
- Sym.toMultisetproof · cited by 51
- Multiset.ext'proof · cited by 31
- Multiset.count_addproof · cited by 23
- Sym.replicateproof · cited by 15
Cited by1
Results whose statement or proof uses this declaration.
- DividedPowers.dpow_sum'proof · cited by 2