ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff

4 sections | 4 files | 39 declarations

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

Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System

imports

Imported by

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower

AddCommGroup

1 file | 16 declarations | 6 Theorems | 3 Definitions | 7 Instances

The principal declarations in this module are: - `instAddCommGroupPrimePowerCompletedCoeffStage` Each coefficient stage \(\mathbb{Z}/\ell^i\mathbb{Z}\) carries its standard addi...

Projection

1 file | 9 declarations | 9 Theorems

The principal declarations in this module are: - `primePowerCompletedCoeffProjection_one` The finite-stage projection sends \(1\) to \(1\). - `primePowerCompletedCoeffProjection...

Ring

1 file | 11 declarations | 5 Theorems | 6 Instances

The principal declarations in this module are: - `instCommRingPrimePowerCompletedCoeffStage` Each finite prime-power coefficient stage is a commutative ring. - `instCommRingPrim...

System

1 file | 3 declarations | 1 Definition | 2 Abbreviations

The principal declarations in this module are: - `primePowerCompletedCoeffSystem` The coefficient inverse system over prime-power group-algebra indices; at index \((a, U)\), its...