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

ink

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

Equations

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

ink

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

Equations

• instFintypeSym' = Quotient.fintype (Vector.Perm.isSetoid α n)

ink

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

Equations

• instFintypeSym = Fintype.ofEquiv (Sym.Sym' α n) (Equiv.symm Sym.symEquivSym')