Theorems · Definition · combinatorics
List.sym
{α : Type u_1} → (n : ℕ) → List α → List (Sym α n)xs.sym n is all unordered n-tuples from the list xs in some order.
- Defined in
- Mathlib.Data.List.Sym
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 48 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Symstatement · cited by 150
Cited by10
Results whose statement or proof uses this declaration.
- List.mem_of_mem_of_mem_symstatement and proof · cited by 1
- List.sym_one_eqstatement and proof · cited by 1
- List.Sublist.symstatement · cited by 1
- List.sym2_eq_sym_twostatement and proof · cited by 0
- List.sym_mapstatement · cited by 0
- List.sym_sublist_sym_consstatement · cited by 0
- List.sym.eq_defstatement · cited by 0
- List.first_mem_of_cons_mem_symstatement and proof · cited by 0
- List.length_symstatement · cited by 0
- List.Nodup.symstatement · cited by 0