ProCGroups/FreeProducts.lean
1import ProCGroups.FreeProducts.UniversalProperty
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/FreeProducts.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# ProCGroups.FreeProducts
14Public wrapper for the `ProCGroups.FreeProducts` folder.
16The concrete inverse-limit construction remains a focused development module;
18-/