ProCGroups/ProC/Quotients.lean

1import ProCGroups.ProC.Quotients.ClosedNormal

2import ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods

3import ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients

4import ProCGroups.ProC.Quotients.LeftQuotientMaps

5import ProCGroups.ProC.Quotients.LeftQuotientProjectionSections

6import ProCGroups.ProC.Quotients.OpenSubgroupSections

8/-

9PUBLIC_PAGE_SNAPSHOT

10generated_at: 2026-05-27T09:47:29+09:00

11lean_source: lean4/ProCGroups/ProC/Quotients.lean

12translation_root: data/translation

13purpose: identifies the local data snapshot used to build pages/

14placement: after imports, never before imports

15-/

16/-!

17# Pro-C groups and open normal quotients

19Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.

20-/