Def Profinite.limitCone

Modification history

2024-05-02 22:40

Mathlib/Topology/Category/Profinite/Basic.lean

chore(Topology/Category): remove `ProfiniteMax` and `CompHausMax` (#12599) …

Modified Profinite.limitCone View on Github →

2023-11-30 10:58

Mathlib/Topology/Category/Profinite/Basic.lean

chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit (#8613) …

Modified Profinite.limitCone View on Github →

2023-05-01 01:58

Mathlib/Topology/Category/Profinite/Basic.lean

feat: port Topology.Category.Profinite.Basic (#3705)

Added Profinite.limitCone View on Github →