Commit 2021-04-30 05:44 f36cc164

View on Github →

chore(topology/category): some lemmas for Profinite functions (#7414) Adds concrete_category and has_forget₂ instances for Profinite, and id_app and comp_app lemmas.

Estimated changes

Modified src/topology/category/Profinite.lean

added theorem Profinite.coe_comp

added theorem Profinite.coe_id

modified def Profinite_to_Top