Def ProfiniteGrp.ofClosedSubgroup

Modification history

2025-04-30 12:59

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

style: further whitespace fixes (#24467) …

Modified ProfiniteGrp.ofClosedSubgroup View on Github →

2024-09-29 13:27

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

feat(Topology/Group): define closed subgroup (#16977) …

Added ProfiniteGrp.ofClosedSubgroup View on Github →