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

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

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

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