Commit 2021-08-25 05:54 bd9622fa

View on Github →

chore(category_theory/Fintype): Fix universe restriction in skeleton (#8855) This removes a universe restriction in the existence of a skeleton for the category Fintype. Once merged, Fintype.skeleton.{u} will be a (small) skeleton for Fintype.{u}, with u any universe parameter.

Estimated changes

Modified src/category_theory/Fintype.lean

added theorem Fintype.comp_apply

added theorem Fintype.id_apply

added theorem Fintype.skeleton.ext

modified def Fintype.skeleton.incl

modified theorem Fintype.skeleton.incl_mk_nat_card

modified theorem Fintype.skeleton.is_skeletal

added def Fintype.skeleton.len

modified def Fintype.skeleton.mk

deleted def Fintype.skeleton.to_nat

modified def Fintype.skeleton