Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup
ProCGroups/FoxDifferential/Completed/ProCIntegerCoefficients/FreeGroup

ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup

3 sections | 3 files | 48 declarations

This aggregate re-exports the following parts of the Fox differential API:

  • Completed.ProCIntegerCoefficients.FreeGroup.Fundamental
import
Imported by

Coordinates

1 file | 12 declarations | 8 Theorems | 4 Definitions
The principal declarations in this module are: - `zcFreeGroupFoxBoundary` The completed Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\). - `zcDifferentialToFre...

Derivative

1 file | 30 declarations | 23 Theorems | 6 Definitions | 1 Abbreviation
The principal declarations in this module are: - `ZCFreeFoxCoordinates` Completed Fox-coordinate vectors with coefficients in \(\mathbb{Z}_C\llbracket H\rrbracket\). - `zcFreeGr...

Fundamental

1 file | 6 declarations | 6 Theorems
The principal declarations in this module are: - `zcFreeGroupFoxBoundary_derivativeVector` The boundary-map form of the completed Fox fundamental formula. - `zcFreeGroupFoxBound...