Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/Source

Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff

1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup
2import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection
3import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring
4import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System
6/-!
7# Fox differential: completed — coefficient rings — prime-power completed group algebra — coeff
9This aggregate re-exports the following parts of the Fox differential API:
11- `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup`
12- `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection`
13- `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring`
14- `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System`
15-/