ProCGroups/ProC/MaximalQuotients.lean

1import ProCGroups.ProC.MaximalQuotients.Definitions

2import ProCGroups.ProC.MaximalQuotients.ResidualCore

3import ProCGroups.ProC.MaximalQuotients.UniversalProperty

5/-

6PUBLIC_PAGE_SNAPSHOT

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

8lean_source: lean4/ProCGroups/ProC/MaximalQuotients.lean

9translation_root: data/translation

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

11placement: after imports, never before imports

13/-!

14# ProCGroups.ProC.MaximalQuotients

16Wrapper for the `ProCGroups.ProC.MaximalQuotients` folder.