ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower

6 sections | 6 files | 83 declarations

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

Completed.CoefficientRings.AugmentationIdealPrimePower.Additive - Completed.CoefficientRings.AugmentationIdealPrimePower.Augmentation - Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv - Completed.CoefficientRings.AugmentationIdealPrimePower.Module - Completed.CoefficientRings.AugmentationIdealPrimePower.Stage - Completed.CoefficientRings.AugmentationIdealPrimePower.SubtypeLinear

imports

Imported by

ProCGroups.FoxDifferential.Completed.CoefficientRings

Additive

1 file | 14 declarations | 6 Theorems | 8 Instances

The principal declarations in this module are: - `instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage` Each finite-stage prime-power augmentation ideal inherit...

Augmentation

1 file | 22 declarations | 15 Theorems | 6 Definitions | 1 Abbreviation

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraAugmentationAddHom` The canonical prime-power augmentation as an additive homomorphism. - `prime...

LimitEquiv

1 file | 16 declarations | 13 Theorems | 3 Definitions

The principal declarations in this module are: - `toPrimePowerCompletedGroupAlgebraAugmentationIdeal` A prime-power augmentation-kernel point determines a compatible family in t...

Module

1 file | 6 declarations | 2 Theorems | 4 Instances

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_smul` The transition map between finite-stage augmentation idea...

Stage

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraStageAugmentationIdeal` The augmentation ideal on one prime-power finite stage. - `primePowerCom...

SubtypeLinear

1 file | 13 declarations | 9 Theorems | 4 Definitions

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraAugmentationIdealAddEquivAddSubgroup` The inverse-limit augmentation ideal is additively equival...