FoxDifferential/Completed/ProCIntegerCoefficients.lean

1import FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation

2import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure

3import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.FiniteStage

4import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Kernel

5import FoxDifferential.Completed.ProCIntegerCoefficients.Core

6import FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental

7import FoxDifferential.Completed.ProCIntegerCoefficients.Naturality

9/-

10PUBLIC_PAGE_SNAPSHOT

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

12lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients.lean

13translation_root: data/translation

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

15placement: after imports, never before imports

16-/

17/-!

18# Completed group algebra coefficients

20This aggregate module re-exports the completed Fox-differential coefficient theory over pro-\(C\) integers, including augmentation, augmentation ideals, naturality, and free-group formulas.

21-/