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

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

- Vector.fintype = Fintype.ofEquiv (Fin n → α) (Equiv.vectorEquivFin α n).symm

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

- instFintypeSym'OfDecidableEq = Quotient.fintype (List.Vector.Perm.isSetoid α n)

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

- instFintypeSymOfDecidableEq = Fintype.ofEquiv (Sym.Sym' α n) Sym.symEquivSym'.symm