@[reducible]

noncomputable def Finite.toFintype {α : Type u_1} (ha : Finite α) : Fintype α

Equations

• ha.toFintype = Fintype.ofFinite α