Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System

2 sections | 6 files | 54 declarations

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

  • Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring
imports
Imported by

Basic

1 file | 14 declarations | 8 Theorems | 2 Definitions | 3 Abbreviations | 1 Instance
The principal declarations in this module are: - `PrimePowerCompletedGroupAlgebraStage` The stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[G/U]\). - `primePowerCompl...

Ring

5 files | 40 declarations | 23 Theorems | 4 Definitions | 13 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup` - `Completed.C...