Theorems · Definition · combinatorics
Finset.sym
{α : Type u_1} → [DecidableEq α] → Finset α → (n : ℕ) → Finset (Sym α n)Lifts a finset to Sym α n. s.sym n is the finset of all unordered tuples of cardinality n
with elements in s.
- Defined in
- Mathlib.Data.Finset.Sym
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 75 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.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by36
Results whose statement or proof uses this declaration.
- Finset.mem_sym_iffstatement and proof · cited by 9
- Finset.symInsertEquivstatement and proof · cited by 6
- DividedPowers.dpow_sumstatement · cited by 2
- DividedPowers.dpow_sum'statement and proof · cited by 2
- Finset.replicate_mem_symstatement · cited by 2
- Finset.sym_eq_emptystatement and proof · cited by 2
- norm_iteratedFDerivWithin_prod_lestatement and proof · cited by 1
- Finset.eq_empty_of_sym_eq_emptystatement and proof · cited by 1
- Finset.Nonempty.symstatement and proof · cited by 1
- Finset.sym_emptystatement · cited by 1
- Finset.sym_filterNe_memstatement and proof · cited by 1
- Finset.sym_monostatement and proof · cited by 1