FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Basic.lean

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

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

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

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

6/-

7PUBLIC_PAGE_SNAPSHOT

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

9lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Basic.lean

10translation_root: data/translation

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

12placement: after imports, never before imports

14/-!

15# Completed coefficient algebras

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