mathlib3 documentation

data.fintype.vector

vector α n and sym α n are fintypes when α is. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def vector.fintype {α : Type u_1} [fintype α] {n : ℕ} :
fintype (vector α n)
Equations
source
@[protected, instance]
def sym.sym'.fintype {α : Type u_1} [decidable_eq α] [fintype α] {n : ℕ} :
fintype (sym.sym' α n)
Equations
source
@[protected, instance]
def sym.fintype {α : Type u_1} [decidable_eq α] [fintype α] {n : ℕ} :
fintype (sym α n)
Equations