Def ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIso

Modification history

2025-02-03 11:50
Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean
feat(Topology/Group): Forgetful functor of ProfiniteGrp reflects isomorphism (#20764) …
Added ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIsoView on Github →