Commit 2020-10-29 07:30 1baf7017

View on Github →

feat(category_theory/Fintype): Adds the category of finite types and its "standard" skeleton. (#4809) This PR adds the category Fintype of finite types, as well as its "standard" skeleton whose objects are fin n.

Estimated changes

Created src/category_theory/Fintype.lean

added def Fintype.incl

added def Fintype.of

added def Fintype.skeleton.incl

added theorem Fintype.skeleton.incl_mk_nat_card

added theorem Fintype.skeleton.is_skeletal

added def Fintype.skeleton.mk

added def Fintype.skeleton.to_nat

added def Fintype.skeleton

added def Fintype

Modified src/data/fintype/basic.lean

added theorem fin.equiv_iff_eq