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

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

@[implicit_reducible]

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

Equations

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

instance Sym.Sym'.instFinite {α : Type u_1} [Finite α] {n : ℕ} : Finite (Sym' α n)

@[implicit_reducible]

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

Equations

• Sym.Sym'.instFintype = { elems := Sym.Sym'.instFintype._aux_1, complete := ⋯ }

instance Sym.instFinite {α : Type u_1} [Finite α] {n : ℕ} : Finite (Sym α n)

@[implicit_reducible]

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

Equations

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