# mathlibdocumentation

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 α] :