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

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

1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation
2import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Map
3import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System
5/-!
6# Fox differential: completed — coefficient rings — prime-power completed group algebra — in class
8This aggregate re-exports the following parts of the Fox differential API:
10- `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation`
11- `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Map`
12- `Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System`
13-/