Commit 2021-05-05 23:47 709c73b2

View on Github →

feat(category_theory/Fintype): some lemmas and Fintype_to_Profinite. (#7491) Adding some lemmas for morphisms on Fintype as functions, as well as Fintype_to_Profinite. Part of the LTE.

Estimated changes

Modified src/category_theory/Fintype.lean

added theorem Fintype.coe_comp

added theorem Fintype.coe_id

added theorem Fintype.comp_apply

added theorem Fintype.id_apply

Modified src/topology/category/Profinite.lean

added def Fintype.discrete_topology

added def Fintype.to_Profinite

added def Profinite.of