Source: ProCGroups.FoxDifferential.Common
1import ProCGroups.FoxDifferential.Common.CrossedDifferential
2import ProCGroups.FoxDifferential.Common.CrossedDifferentialModule
3import ProCGroups.FoxDifferential.Common.FiniteFamilyLinearMap
4import ProCGroups.FoxDifferential.Common.FoxBoundary
5import ProCGroups.FoxDifferential.Common.FreeCrossedDifferential
6import ProCGroups.FoxDifferential.Common.Jacobian
8/-!
9# Common Fox-differential interface
11This aggregate collects the algebraic interface shared by the discrete and completed theories:
12bundled crossed homomorphisms, their universal differential modules, Fox boundary identities,
13free-source differentials, finite-family linear maps, and Jacobian constructions. It does not
14choose a completion topology or a finite-stage coefficient system.
15-/