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.

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