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

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower

6 sections | 29 files | 203 declarations

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

  • Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System
imports
Imported by

Augmentation

1 file | 3 declarations | 2 Theorems | 1 Definition
The principal declarations in this module are: - `primePowerCompletedGroupAlgebraAugmentation` The prime-power completed group algebra carries a canonical augmentation to the co...

Basic

5 files | 19 declarations | 12 Theorems | 4 Definitions | 3 Abbreviations
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation` - `Completed.Coeffic...

Coeff

5 files | 39 declarations | 20 Theorems | 4 Definitions | 2 Abbreviations | 13 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup` - `Completed.Coeffic...

InClass

10 files | 76 declarations | 44 Theorems | 12 Definitions | 3 Abbreviations | 17 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation` - `Completed.Coeff...

Module

1 file | 12 declarations | 7 Theorems | 1 Definition | 4 Instances
The principal declarations in this module are: - `primePowerCompletedCoeffToGroupAlgebra` The coefficient inverse limit maps canonically into the completed group algebra by taki...

System

7 files | 54 declarations | 31 Theorems | 6 Definitions | 3 Abbreviations | 14 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic` - `Completed.CoefficientRi...