Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients
ProCGroups/FoxDifferential/Completed/ProCIntegerCoefficients/Source

Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients

1import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation
2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal
3import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Core
4import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup
5import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Naturality
7/-!
8# Fox differential: completed — \(\mathbb{Z}_C\) coefficients
10This aggregate re-exports the following parts of the Fox differential API:
12- `Completed.ProCIntegerCoefficients.Augmentation`
13- `Completed.ProCIntegerCoefficients.AugmentationIdeal`
14- `Completed.ProCIntegerCoefficients.Core`
15- `Completed.ProCIntegerCoefficients.FreeGroup`
16- `Completed.ProCIntegerCoefficients.Naturality`
17-/