FoxDifferential/Completed/FiniteStage.lean
1import FoxDifferential.Completed.FiniteStage.Basic
2import FoxDifferential.Completed.FiniteStage.BoundaryCycles
3import FoxDifferential.Completed.FiniteStage.BoundaryCycleHom
4import FoxDifferential.Completed.FiniteStage.RelationModule
5import FoxDifferential.Completed.FiniteStage.RelationAction
6import FoxDifferential.Completed.FiniteStage.RelationSubmodule
7import FoxDifferential.Completed.FiniteStage.BoundaryQuotient
8import FoxDifferential.Completed.FiniteStage.SemidirectCycles
9import FoxDifferential.Completed.FiniteStage.BoundarySubgroups
10import FoxDifferential.Completed.FiniteStage.RelationRealization
11import FoxDifferential.Completed.FiniteStage.RelationIdeal
12import FoxDifferential.Completed.FiniteStage.SourceBoundary
13import FoxDifferential.Completed.FiniteStage.RelationIdealDerivative
14import FoxDifferential.Completed.FiniteStage.CoeffMap.Augmentation
15import FoxDifferential.Completed.FiniteStage.CoeffMap.Semidirect
16import FoxDifferential.Completed.FiniteStage.CoeffMap.Boundary
17import FoxDifferential.Completed.FiniteStage.CoeffMap.BoundaryCycles
18import FoxDifferential.Completed.FiniteStage.MagnusQuotient
19import FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.Index
20import FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.LimitMap
21import FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.Representatives
22import FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Target
23import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.CompletedSource
24import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.CompletedTarget
25import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Limit
26import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Vector
27import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.OnGroup.Vector
28import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.OnGroup.Projection
29import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Fundamental
30import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.GroupLike
31import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Mul
32import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.SpecialValues
33import FoxDifferential.Completed.FiniteStage.PrimePower.System.Basic
34import FoxDifferential.Completed.FiniteStage.PrimePower.System.Semidirect
35import FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.AddCommGroup
36import FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.CoeffMap
37import FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.Mul
38import FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.Semidirect
39import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Boundary
40import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Relators
41import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Rules
42import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Quotient.Fundamental
43import FoxDifferential.Completed.FiniteStage.Stage.Fundamental.Formula
44import FoxDifferential.Completed.FiniteStage.Stage.KernelIdeal
45import FoxDifferential.Completed.FiniteStage.Stage.Naturality
46import FoxDifferential.Completed.FiniteStage.Stage.Semidirect
47import FoxDifferential.Completed.FiniteStage.Stage.Source
48import FoxDifferential.Completed.FiniteStage.TargetMap
49import FoxDifferential.Completed.FiniteStage.Bifiltered.Transition
50import FoxDifferential.Completed.FiniteStage.Bifiltered.System
51import FoxDifferential.Completed.FiniteStage.Bifiltered.InverseSystem
53/-
54PUBLIC_PAGE_SNAPSHOT
55generated_at: 2026-05-27T09:47:29+09:00
56lean_source: lean4/FoxDifferential/Completed/FiniteStage.lean
57translation_root: data/translation
58purpose: identifies the local data snapshot used to build pages/
59placement: after imports, never before imports
60-/
61/-!
62# Finite-stage completed Fox calculus
64Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.
65-/