Theorems · Definition · combinatorics
Multiset.powersetCardAux
{α : Type u_1} → ℕ → List α → List (Multiset α)Helper function for powersetCard. Given a list l, powersetCardAux n l is the list
of sublists of length n, as multisets.
- Defined in
- Mathlib.Data.Multiset.Powerset
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement · cited by 2,627
- Multiset.ofListproof · cited by 290
- List.sublistsLenAuxproof · cited by 5
Cited by9
Results whose statement or proof uses this declaration.
- Multiset.powersetCardproof · cited by 29
- Multiset.powersetCard_consproof · cited by 4
- Multiset.powersetCardAux_eq_map_coestatement · cited by 4
- Multiset.powersetCardAux_zerostatement · cited by 2
- Multiset.powersetCardAux_consstatement · cited by 2
- Multiset.powersetCardAux_permstatement and proof · cited by 0
- Multiset.powersetCard_coe'statement · cited by 0
- Multiset.mem_powersetCardAuxstatement · cited by 0
- Multiset.powersetCardAux_nilstatement · cited by 0