Source: ProCGroups.FoxDifferential.Completed.Continuous

1import ProCGroups.FoxDifferential.Completed.Continuous.Automorphism

2import ProCGroups.FoxDifferential.Completed.Continuous.ChainRule

3import ProCGroups.FoxDifferential.Completed.Continuous.Free

4import ProCGroups.FoxDifferential.Completed.Continuous.Naturality

5import ProCGroups.FoxDifferential.Completed.Continuous.SemidirectKernelBasis

6import ProCGroups.FoxDifferential.Completed.Continuous.TailExactness

7import ProCGroups.FoxDifferential.Completed.Continuous.TopologicalGeneration

8import ProCGroups.FoxDifferential.Completed.Continuous.Topology

9import ProCGroups.FoxDifferential.Completed.Continuous.Universal

10import ProCGroups.FoxDifferential.Completed.Continuous.PresentedCoordinates

11import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates

12import ProCGroups.FoxDifferential.Completed.Continuous.Magnus

14/-!

15# Continuous completed Fox calculus

17This aggregate imports the topology and continuity of completed Fox coordinates, their naturality

18and chain rules, free-source and universal constructions, topological-generation formulas,

19semidirect-kernel bases, automorphism formulas, and the resulting tail exactness theorems. The

20common algebraic `CrossedHom` interface is supplied by `FoxDifferential.Common`; finite-stage and

21completion-specific implementations are collected here.