Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.CoefficientRings
ProCGroups/FoxDifferential/Completed/CoefficientRings

ProCGroups.FoxDifferential.Completed.CoefficientRings

4 sections | 51 files | 427 declarations

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

  • Completed.CoefficientRings.AugmentationIdealPrimePower - Completed.CoefficientRings.CompletedGroupAlgebra - Completed.CoefficientRings.CompletedGroupAlgebraModN - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower
imports
Imported by

AugmentationIdealPrimePower

7 files | 83 declarations | 49 Theorems | 17 Definitions | 4 Abbreviations | 13 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.AugmentationIdealPrimePower.Additive` - `Completed.CoefficientRings.Augm...

CompletedGroupAlgebra

1 file | 22 declarations | 11 Theorems | 7 Definitions | 4 Abbreviations
The principal declarations in this module are: - `CompletedGroupAlgebraIndexInClass` The index set for a completed group algebra over finite quotients belonging to a class `C`. ...

CompletedGroupAlgebraModN

13 files | 119 declarations | 69 Theorems | 22 Definitions | 11 Abbreviations | 17 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation` - `Completed.CoefficientRings.Co...

CompletedGroupAlgebraPrimePower

30 files | 203 declarations | 116 Theorems | 28 Definitions | 11 Abbreviations | 48 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation` - `Completed.CoefficientRi...