FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN.lean

1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation

2import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal

3import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.CoeffMap

4import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup

5import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation

6import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap

8/-

9PUBLIC_PAGE_SNAPSHOT

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

11lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN.lean

12translation_root: data/translation

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

14placement: after imports, never before imports

16/-!

17# Completed coefficient algebras

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