Def ProfiniteGrp.limitConePtAux

Modification history

2024-09-29 08:12
Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean
feat(Topology/Group/Profinite): limits in the category of profinite groups (#16976) …
Added ProfiniteGrp.limitConePtAuxView on Github →