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

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System

2 sections | 6 files | 54 declarations

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

  • Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring
imports
Imported by

Basic

1 file | 17 declarations | 11 Theorems | 4 Definitions | 2 Abbreviations
The principal declarations in this module are: - `PrimePowerCompletedGroupAlgebraStageInClass` The class-restricted prime-power stage at index \((a,U)\), namely \((\mathrm{ZMod}...

Ring

5 files | 37 declarations | 22 Theorems | 2 Definitions | 13 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup` - `Com...