FoxDifferential/Completed/FiniteStage/CoeffMap.lean

1import FoxDifferential.Completed.FiniteStage.CoeffMap.Augmentation

2import FoxDifferential.Completed.FiniteStage.CoeffMap.Semidirect

3import FoxDifferential.Completed.FiniteStage.CoeffMap.Boundary

4import FoxDifferential.Completed.FiniteStage.CoeffMap.BoundaryCycles

6/-

7PUBLIC_PAGE_SNAPSHOT

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

9lean_source: lean4/FoxDifferential/Completed/FiniteStage/CoeffMap.lean

10translation_root: data/translation

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

12placement: after imports, never before imports

13-/

14/-!

15# Finite-stage completed Fox calculus

17Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

18-/