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

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

4 sections | 4 files | 37 declarations

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

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

AddCommGroup

1 file | 14 declarations | 6 Theorems | 1 Definition | 7 Instances
The principal declarations in this module are: - `instAddCommGroupPrimePowerCompletedGroupAlgebraInClass` The class-indexed prime-power completion inherits an additive commutati...

GroupLike

1 file | 4 declarations | 3 Theorems | 1 Definition
The principal declarations in this module are: - `primePowerCompletedGroupAlgebraOfInClass` The class-restricted completed group-algebra element represented by a group element. ...

Multiplicative

1 file | 11 declarations | 5 Theorems | 6 Instances
The principal declarations in this module are: - `coe_one_primePowerCompletedGroupAlgebraInClass` The multiplicative identity in the class-indexed prime-power completed group al...

Projection

1 file | 8 declarations | 8 Theorems
The principal declarations in this module are: - `primePowerCompletedGroupAlgebraProjectionInClass_one` The finite-stage projection sends \(1\) to \(1\). - `primePowerCompletedG...