mathlib documentation

data.fintype.small

All finite types are small. #

That is, any α with [fintype α] is equivalent to a type in any universe.

@[instance]
def small_of_fintype (α : Type v) [fintype α] :