Commit 2023-04-10 19:55 71bb33c5

View on Github →

feat: port CategoryTheory.Fintype (#3365)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/FintypeCat.lean

added theorem FintypeCat.Skeleton.ext

added def FintypeCat.Skeleton.incl

added theorem FintypeCat.Skeleton.incl_mk_nat_card

added theorem FintypeCat.Skeleton.is_skeletal

added def FintypeCat.Skeleton.len

added def FintypeCat.Skeleton.mk

added def FintypeCat.Skeleton

added theorem FintypeCat.comp_apply

added def FintypeCat.equivEquivIso

added theorem FintypeCat.hom_ext

added theorem FintypeCat.id_apply

added def FintypeCat.incl

added def FintypeCat.of

added def FintypeCat