# Documentation

Mathlib.Data.Fintype.Small

# All finite types are small. #

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

instance small_of_fintype (α : Type v) [inst : ] :
Equations