ProCGroups/ProC/OpenNormalSubgroups.lean
1import ProCGroups.ProC.OpenNormalSubgroups.Basic
2import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
3import ProCGroups.ProC.OpenNormalSubgroups.ClosedAndCosets
4import ProCGroups.ProC.OpenNormalSubgroups.ClosedCommutator
5import ProCGroups.ProC.OpenNormalSubgroups.CountableChains
6import ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies
7import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
8import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
9import ProCGroups.ProC.OpenNormalSubgroups.Separation
11/-
12PUBLIC_PAGE_SNAPSHOT
13generated_at: 2026-05-27T09:47:29+09:00
14lean_source: lean4/ProCGroups/ProC/OpenNormalSubgroups.lean
15translation_root: data/translation
16purpose: identifies the local data snapshot used to build pages/
17placement: after imports, never before imports
18-/
19/-!
20# ProCGroups.ProC.OpenNormalSubgroups
22Wrapper for the `ProCGroups.ProC.OpenNormalSubgroups` folder.
23-/