FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower.lean

1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation

2import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation

3import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap

4import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.AllFinite

5import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.Coeff

6import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup

7import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection

8import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring

9import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System

10import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation

11import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Map

12import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic

13import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup

14import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.GroupLike

15import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Multiplicative

16import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection

17import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module

18import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic

19import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup

20import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike

21import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative

22import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection

25PUBLIC_PAGE_SNAPSHOT

26generated_at: 2026-05-27T09:47:29+09:00

27lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower.lean

28translation_root: data/translation

29purpose: identifies the local data snapshot used to build pages/

30placement: after imports, never before imports

32/-!

33# Completed coefficient algebras

35Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.