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

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring

4 sections | 4 files | 40 declarations

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

  • Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection
imports
Imported by

AddCommGroup

1 file | 16 declarations | 6 Theorems | 3 Definitions | 7 Instances
The principal declarations in this module are: - `instAddCommGroupPrimePowerCompletedGroupAlgebraStage` Each finite prime-power group-algebra stage carries its standard additive...

GroupLike

1 file | 6 declarations | 5 Theorems | 1 Definition
The principal declarations in this module are: - `primePowerCompletedGroupAlgebraOf` The canonical map sends a group element to its compatible family of prime-power finite-stage...

Multiplicative

1 file | 11 declarations | 5 Theorems | 6 Instances
The principal declarations in this module are: - `instRingPrimePowerCompletedGroupAlgebraStage` Each finite prime-power group-algebra stage carries its standard ring structure. ...

Projection

1 file | 7 declarations | 7 Theorems
The principal declarations in this module are: - `primePowerCompletedGroupAlgebraProjection_natCast` The finite-stage projection preserves natural number casts. - `primePowerCom...