ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal

4 sections | 4 files | 63 declarations

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

Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic - Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure - Completed.ProCIntegerCoefficients.AugmentationIdeal.FiniteStage - Completed.ProCIntegerCoefficients.AugmentationIdeal.Kernel

imports

Imported by

ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients

Basic

1 file | 11 declarations | 8 Theorems | 3 Definitions

The principal declarations in this module are: - `zcCompletedGroupAlgebraStandardAugmentationIdeal` The algebraic ideal generated by the standard completed augmentation generato...

Closure

1 file | 2 declarations | 2 Theorems

The principal declarations in this module are: - `zcCompletedGroupAlgebraStageAugmentationIdeal_mem_projection_standard` Every finite-stage augmentation-ideal element is the pro...

FiniteStage

1 file | 20 declarations | 10 Theorems | 9 Definitions | 1 Abbreviation

The principal declarations in this module are: - `zcCompletedGroupAlgebraStageAugmentationIdeal` The augmentation ideal in one finite stage of \(\mathbb{Z}_C\llbracket H\rrbrack...

Kernel

1 file | 30 declarations | 24 Theorems | 6 Definitions

The principal declarations in this module are: - `groupAlgebraMapDomainKernelAugmentationIdeal` The ideal in \(R[A]\) generated by \([k]-1\) for \(k \in \ker f\). - `groupAlgebr...