# 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 `Multiset (List α)` is provided. This function is applied to the `Finset.powerset` of `Finset.univ`.

source
def Multiset.lists {α : Type u_1} :
Multiset α → Multiset (List α)

Given a `m : Multiset α`, we form the `Multiset` of `l : List α` with the property `⟦l⟧ = m`.

Equations

- s.lists = Quotient.liftOn s (fun (l : List α) => ↑l.permutations) ⋯

Instances For

source
@[simp]
theorem Multiset.lists_coe {α : Type u_1} (l : List α) :
(↑l).lists = ↑l.permutations
source
@[simp]
theorem Multiset.lists_nodup_finset {α : Type u_1} (l : Finset α) :
l.val.lists.Nodup
source
@[simp]
theorem Multiset.mem_lists_iff {α : Type u_1} (s : Multiset α) (l : List α) :
l ∈ s.lists ↔ s = ⟦l⟧
source
instance fintypeNodupList {α : Type u_1} [Fintype α] :
Fintype { l : List α // l.Nodup }
Equations

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