Documentation

Mathlib.Data.Fintype.Vector

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

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