FoxDifferential.lean
1import FoxDifferential.Common.CrossedDifferential
2import FoxDifferential.Common.CrossedDifferentialModule
3import FoxDifferential.Common.FiniteFamilyLinearMap
4import FoxDifferential.Common.FoxBoundary
5import FoxDifferential.Common.FreeCrossedDifferential
6import FoxDifferential.Common.Jacobian
7import FoxDifferential.Discrete.Absolute
8import FoxDifferential.Discrete.DifferentialModule.Boundary
9import FoxDifferential.Discrete.FoxCalculus.Boundary
10import FoxDifferential.Discrete.FoxCalculus.Coordinates
11import FoxDifferential.Discrete.FoxCalculus.Derivative
12import FoxDifferential.Discrete.FoxCalculus.Semidirect
13import FoxDifferential.Discrete.FoxCalculus.Universal
14import FoxDifferential.Discrete.FreeExpansion
15import FoxDifferential.Discrete.Jacobian.Automorphism
16import FoxDifferential.Discrete.Naturality
17import FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation
18import FoxDifferential.Discrete.KernelBoundary.Basic
19import FoxDifferential.Discrete.KernelBoundary.Homology
20import FoxDifferential.Discrete.KernelBoundary.Quotient
21import FoxDifferential.Discrete.KernelBoundary.MagnusKernel
22import FoxDifferential.Completed.DifferentialModule.Identity
23import FoxDifferential.Completed.DifferentialModule.Map.Comap
24import FoxDifferential.Completed.DifferentialModule.Map.GroupLike
25import FoxDifferential.Completed.DifferentialModule.Map.Limit
26import FoxDifferential.Completed.DifferentialModule.Map.Stage
27import FoxDifferential.Completed.DifferentialModule.Map.Surjective
28import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Basic
29import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental
30import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Surjective
31import FoxDifferential.Completed.Continuous.Automorphism
32import FoxDifferential.Completed.Continuous.Free.DiscreteGenerators
33import FoxDifferential.Completed.Continuous.Free.Rules
34import FoxDifferential.Completed.Continuous.Topology
35import FoxDifferential.Completed.Continuous.ChainRule.Basic
36import FoxDifferential.Completed.Continuous.ChainRule.Iterated
37import FoxDifferential.Completed.Continuous.Naturality
38import FoxDifferential.Completed.Continuous.TailExactness
39import FoxDifferential.Completed.Continuous.TopologicalGeneration
40import FoxDifferential.Completed.Continuous.Universal.Basic
41import FoxDifferential.Completed.Continuous.Universal.FiniteStage
42import FoxDifferential.Completed.Continuous.Universal.NaturalTopology
43import FoxDifferential.Completed.Continuous.Universal.System
44import FoxDifferential.Completed.Continuous.SemidirectKernelBasis
45import FoxDifferential.Completed.FreeProC.SemidirectLift
46import FoxDifferential.Completed.FreeProC.Uniqueness.Derivative
47import FoxDifferential.Completed.FreeProC.Uniqueness.Existence
48import FoxDifferential.Completed.FreeProC.Uniqueness.Lift
49import FoxDifferential.Completed.FreeProC.Uniqueness.Morphism
50import FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom
51import FoxDifferential.Completed.FreeProC.Density
52import FoxDifferential.Completed.FreeProC.QuotientKernelBasis
53import FoxDifferential.Completed.FreeProC.CofinalQuotientKernelBasis
54import FoxDifferential.Completed.FreeProC.FiniteQuotientStages
55import FoxDifferential.Completed.FreeProC.SemidirectKernelBasis
56import FoxDifferential.RightDerivative.GeometricSeries
57import FoxDifferential.RightDerivative.Basic
58import FoxDifferential.RightDerivative.Semidirect
59import FoxDifferential.RightDerivative.IntegerPower
60import FoxDifferential.RightDerivative.CommutatorFormula
62/-
63PUBLIC_PAGE_SNAPSHOT
64generated_at: 2026-05-27T09:47:29+09:00
65lean_source: lean4/FoxDifferential.lean
66translation_root: data/translation
67purpose: identifies the local data snapshot used to build pages/
68placement: after imports, never before imports
69-/
70/-!
71# Fox differential calculus
73Public entry point for the Fox-differential calculus library. The library contains crossed
74differentials, Fox derivatives on free groups and group rings, Fox boundaries, Jacobians,
75completed/profinite Fox differentials, and right Fox-derivative formulas.
77It may import `ProCGroups`, `ReidemeisterSchreier`, and `CompletedGroupAlgebra`. The downstream
78modules `CrowellExactSequence` and `MetabelianProductCentralizer` are intentionally not imported.
79-/