mathlib

f36cc164 - chore(topology/category): some lemmas for Profinite functions (#7414)

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.