Vector α n and Sym α n are fintypes when α is.

@[implicit_reducible]

instance Vector.fintype {α : Type u_1} [Fintype α] {n : ℕ} : Fintype (List.Vector α n)

Equations

• Vector.fintype = { elems := Finset.map { toFun := ⇑(Equiv.vectorEquivFin α n).symm, inj' := ⋯ } Finset.univ, complete := ⋯ }

@[implicit_reducible]

instance instFintypeSym'OfDecidableEq {α : Type u_1} [DecidableEq α] [Fintype α] {n : ℕ} : Fintype (Sym.Sym' α n)

Equations

• instFintypeSym'OfDecidableEq = { elems := instFintypeSym'OfDecidableEq._aux_1, complete := ⋯ }

@[implicit_reducible]

instance instFintypeSymOfDecidableEq {α : Type u_1} [DecidableEq α] [Fintype α] {n : ℕ} : Fintype (Sym α n)

Equations

• instFintypeSymOfDecidableEq = { elems := Finset.map { toFun := ⇑Sym.symEquivSym'.symm, inj' := ⋯ } Finset.univ, complete := ⋯ }