FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System.lean

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

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

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

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

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

7/-

8PUBLIC_PAGE_SNAPSHOT

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

10lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System.lean

11translation_root: data/translation

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

13placement: after imports, never before imports

15/-!

16# Completed coefficient algebras

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