Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.Residue
ProCGroups/FoxDifferential/Completed/Residue

ProCGroups.FoxDifferential.Completed.Residue

2 sections | 7 files | 42 declarations

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

  • Completed.Residue.Core - Completed.Residue.FreeGroup
imports
Imported by

Core

1 file | 15 declarations | 7 Theorems | 6 Definitions | 2 Abbreviations
The principal declarations in this module are: - `ResidueGroupRing` The residue group ring \((\mathbb{Z}/n\mathbb{Z})[H]\). - `residueGroupRingScalar` The coefficient homomorphi...

FreeGroup

6 files | 27 declarations | 18 Theorems | 8 Definitions | 1 Abbreviation
This aggregate re-exports the following parts of the Fox differential API: - `Completed.Residue.FreeGroup.Basic` - `Completed.Residue.FreeGroup.Boundary` - `Completed.Residue.Fr...