Yamaguchi Lean 4 Library
ProCGroups/ProC.lean
ProCGroups/ProC/Source

ProCGroups/ProC.lean

1import ProCGroups.ProC.Category.Basic
2import ProCGroups.ProC.Category.Pullbacks
3import ProCGroups.ProC.Category.Pushouts
4import ProCGroups.ProC.GroupPredicate
5import ProCGroups.ProC.GroupPredicates.Basic
6import ProCGroups.ProC.GroupPredicates.Standard
7import ProCGroups.ProC.GroupPredicates.Abelian
8import ProCGroups.ProC.Kernels
9import ProCGroups.ProC.MaximalQuotients.Definitions
10import ProCGroups.ProC.MaximalQuotients.ResidualCore
11import ProCGroups.ProC.MaximalQuotients.UniversalProperty
12import ProCGroups.ProC.OpenNormalSubgroups.Basic
13import ProCGroups.ProC.OpenNormalSubgroups.CountableChains
14import ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies
15import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
16import ProCGroups.ProC.OpenNormalSubgroups.ClosedCommutator
17import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
18import ProCGroups.ProC.OpenNormalSubgroups.Separation
19import ProCGroups.ProC.Quotients.ClosedNormal
20import ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods
21import ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients
22import ProCGroups.ProC.Quotients.LeftQuotientMaps
23import ProCGroups.ProC.Quotients.LeftQuotientProjectionSections
24import ProCGroups.ProC.Quotients.OpenSubgroupSections
25import ProCGroups.ProC.Subgroups.Products
26import ProCGroups.Profinite.Basic
27import ProCGroups.Profinite.MathlibBridge
29/-
30PUBLIC_PAGE_SNAPSHOT
31generated_at: 2026-05-27T09:47:29+09:00
32lean_source: lean4/ProCGroups/ProC.lean
33translation_root: data/translation
34purpose: identifies the local data snapshot used to build pages/
35placement: after imports, never before imports
36-/
37/-!
38# Pro-C groups and open normal quotients
40Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
41-/