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

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic

2 sections | 4 files | 19 declarations

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

  • Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap
imports
Imported by

Augmentation

1 file | 11 declarations | 5 Theorems | 4 Definitions | 2 Abbreviations
The principal declarations in this module are: - `modNCompletedGroupAlgebraCoeffMap` The modulus-direction map on residue-coefficient completed group algebras. - `modNCompletedG...

StageCoeffMap

3 files | 8 declarations | 7 Theorems | 1 Abbreviation
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap` - `Completed.Coefficien...