ProCGroups/Topologies.lean
1import ProCGroups.Topologies.Conjugation
2import ProCGroups.Topologies.ContinuousMonoidHom
3import ProCGroups.Topologies.ContinuousMulEquiv
4import ProCGroups.Topologies.FullSubgroupTopology.QuotientFormation
5import ProCGroups.Topologies.FullSubgroupTopology.QuotientVariety
6import ProCGroups.Topologies.OpenSubgroup
7import ProCGroups.Topologies.QuotientMaps
8import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
10/-
11PUBLIC_PAGE_SNAPSHOT
12generated_at: 2026-05-27T09:47:29+09:00
13lean_source: lean4/ProCGroups/Topologies.lean
14translation_root: data/translation
15purpose: identifies the local data snapshot used to build pages/
16placement: after imports, never before imports
17-/
18/-!
19# ProCGroups.Topologies
21Wrapper for the `ProCGroups.Topologies` folder.
22-/