# Fintype instance for nodup lists #

The subtype of `{l : List α // l.nodup}`

over a `[Fintype α]`

admits a `Fintype`

instance.

## Implementation details #

To construct the `Fintype`

instance, a function lifting a `Multiset α`

to the `Finset (list α)`

that can construct it is provided.
This function is applied to the `Finset.powerset`

of `Finset.univ`

.

In general, a `DecidableEq`

instance is not necessary to define this function,
but a proof of `(List.permutations l).nodup`

is required to avoid it,
which is a TODO.

The `Finset`

of `l : List α`

that, given `m : Multiset α`

, have the property `⟦l⟧ = m`

.

## Equations

- One or more equations did not get rendered due to their size.

@[simp]

@[simp]

theorem
Multiset.mem_lists_iff
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(l : List α)
:

l ∈ Multiset.lists s ↔ s = Quotient.mk (List.isSetoid α) l

instance
fintypeNodupList
{α : Type u_1}
[inst : DecidableEq α]
[inst : Fintype α]
:

Fintype { l // List.Nodup l }

## Equations

- One or more equations did not get rendered due to their size.