# Zulip Chat Archive

## Stream: general

### Topic: n-permutations of a list

#### Vaibhav Karve (Jul 29 2020 at 20:34):

We already have `list.permutations : list A -> list (list A)`

. Is there a version of this that takes an argument `n : nat`

and gives all possible ~~n-permutations ~~ **n-combinations** (sublists of size `n`

without ordering)? Should I be using `list.sublists`

and then filtering for the ones with length `n`

?

Edit: I changed permutations to combinations.

#### Mario Carneiro (Jul 29 2020 at 20:39):

sublists and permutations are not the same thing. Are reorderings being considered?

#### Mario Carneiro (Jul 29 2020 at 20:48):

```
namespace list
def n_sublists_aux {α} : ℕ → list α → (list α → list α) → list (list α) → list (list α)
| 0 _ f r := f [] :: r
| (n+1) [] f r := r
| (n+1) (a::l) f r := n_sublists_aux n l (λ x, f (a :: x)) (n_sublists_aux (n+1) l f r)
def n_sublists {α} (n : ℕ) (l : list α) : list (list α) := n_sublists_aux n l id []
#eval n_sublists 2 [1,2,3,4,5]
-- [[1, 2], [1, 3], [1, 4], [1, 5], [2, 3], [2, 4], [2, 5], [3, 4], [3, 5], [4, 5]]
end list
```

#### Mario Carneiro (Jul 29 2020 at 20:48):

I leave the proof of correctness as an exercise for the reader

#### Patrick Massot (Jul 29 2020 at 20:49):

Mario Carneiro said:

I leave the proof of correctness as an exercise for the reader

This is also my favorite tactic.

#### Mario Carneiro (Jul 29 2020 at 20:50):

`by laziness`

#### Vaibhav Karve (Jul 29 2020 at 20:51):

Yeah, I meant combinations. I fixed the question.

#### Vaibhav Karve (Jul 29 2020 at 20:55):

I think it would be nice to have a function for n-combinations as well as n-permutaions in mathlib?

#### Mario Carneiro (Jul 29 2020 at 21:09):

Yes, that function should be in `data.list.defs`

Last updated: May 10 2021 at 00:31 UTC