ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass

4 sections | 4 files | 50 declarations

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

Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup - Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation

imports

Imported by

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN

AddCommGroup

1 file | 20 declarations | 12 Theorems | 8 Instances

The principal declarations in this module are: - `coe_zero_modNCompletedGroupAlgebraInClass` The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambien...

Augmentation

1 file | 6 declarations | 5 Theorems | 1 Definition

The principal declarations in this module are: - `modNCompletedGroupAlgebraStageAugmentationInClass` The augmentation on one class-restricted residue-coefficient finite stage. -...

Basic

1 file | 17 declarations | 8 Theorems | 5 Definitions | 4 Abbreviations

The principal declarations in this module are: - `ModNCompletedCoeff` The coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) used in one residue-coefficient stage. - `ModNCompletedGrou...

StageCoeffMap

1 file | 7 declarations | 6 Theorems | 1 Abbreviation

The principal declarations in this module are: - `modNCompletedGroupAlgebraStageCoeffMapInClass` The coefficient reduction map on one class-restricted finite quotient stage \(G/...