Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-15 05:43 e42af8da

View on Github →

refactor(topology/category/Profinite): define Profinite as a subcategory of CompHaus (#8314) This adjusts the definition of Profinite to explicitly be a subcategory of CompHaus rather than a subcategory of Top which embeds into CompHaus. Essentially this means it's easier to construct an element of Profinite from an element of CompHaus.

Estimated changes