mathlib3 documentation

data.fintype.array

array n α is a fintype when α is. #

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

source
@[protected, instance]
def d_array.fintype {n : ℕ} {α : fin n → Type u_1} [Π (n : fin n), fintype (α n)] :
fintype (d_array n α)
Equations
source
@[protected, instance]
def array.fintype {n : ℕ} {α : Type u_1} [fintype α] :
fintype (array n α)
Equations