FoxDifferential/Completed/CoefficientRings.lean
1import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Additive
2import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Augmentation
3import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv
4import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Module
5import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Stage
6import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.SubtypeLinear
7import CompletedGroupAlgebra.Basic.AllFinite.Stage
8import CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps
9import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra
10import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation
11import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal
12import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.CoeffMap
13import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup
14import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation
15import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap
16import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation
17import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation
18import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap
19import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.AllFinite
20import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.Coeff
21import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup
22import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection
23import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring
24import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System
25import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation
26import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Map
27import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic
28import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup
29import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.GroupLike
30import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Multiplicative
31import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
32import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module
33import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic
34import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup
35import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike
36import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative
37import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection
39/-
40PUBLIC_PAGE_SNAPSHOT
41generated_at: 2026-05-27T09:47:29+09:00
42lean_source: lean4/FoxDifferential/Completed/CoefficientRings.lean
43translation_root: data/translation
44purpose: identifies the local data snapshot used to build pages/
45placement: after imports, never before imports
46-/
47/-!
48# Completed coefficient algebras
50Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
51-/