ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN

5 sections | 12 files | 119 declarations

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

Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation - Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal - Completed.CoefficientRings.CompletedGroupAlgebraModN.CoeffMap - Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass - Completed.CoefficientRings.CompletedGroupAlgebraModN.System

imports

Imported by

ProCGroups.FoxDifferential.Completed.CoefficientRings

Augmentation

1 file | 9 declarations | 6 Theorems | 3 Definitions

The principal declarations in this module are: - `modNCompletedGroupAlgebraStageAugmentation` The augmentation on one residue-coefficient finite stage. - `modNCompletedGroupAlge...

AugmentationIdeal

1 file | 20 declarations | 10 Theorems | 7 Definitions | 3 Abbreviations

The principal declarations in this module are: - `modNCompletedGroupAlgebraStageAugmentationIdeal` The augmentation ideal on one residue-coefficient finite stage. - `modNComplet...

CoeffMap

1 file | 5 declarations | 3 Theorems | 2 Definitions

The principal declarations in this module are: - `modNCompletedCoeffMap` The coefficient reduction map \(\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}\) attached to a divisi...

InClass

This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup` - `Completed.Coefficient...

System

This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap`