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

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass

3 sections | 9 files | 76 declarations

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

  • Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Map - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System
imports
Imported by

Augmentation

1 file | 15 declarations | 6 Theorems | 4 Definitions | 1 Abbreviation | 4 Instances
The principal declarations in this module are: - `primePowerCompletedCoeffSystemInClass` The class-restricted coefficient inverse system indexed by \(i = (a,U)\), whose coeffici...

Map

1 file | 7 declarations | 5 Theorems | 2 Definitions
The principal declarations in this module are: - `primePowerCompletedGroupAlgebraMapStageInClass` The finite-stage component of a class-restricted prime-power completed group-al...

System

7 files | 54 declarations | 33 Theorems | 6 Definitions | 2 Abbreviations | 13 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic` - `Completed.Coeff...