ProCGroups/NormalSubgroups/SimpleQuotients.lean

1import ProCGroups.NormalSubgroups.SimpleQuotients.Algebraic

2import ProCGroups.NormalSubgroups.SimpleQuotients.Compactness

3import ProCGroups.NormalSubgroups.SimpleQuotients.FiniteIntersections

5/-

6PUBLIC_PAGE_SNAPSHOT

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

8lean_source: lean4/ProCGroups/NormalSubgroups/SimpleQuotients.lean

9translation_root: data/translation

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

11placement: after imports, never before imports

13/-!

14# ProCGroups.NormalSubgroups.SimpleQuotients

16Wrapper for the `ProCGroups.NormalSubgroups.SimpleQuotients` folder.