mathlib documentation

data.fintype.small

All finite types are small. #

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

source
@[protected, instance]
def small_of_fintype (α : Type v) [fintype α] :
small α