FoxDifferential/Completed/Continuous.lean

1import FoxDifferential.Completed.Continuous.Automorphism

2import FoxDifferential.Completed.Continuous.Free.DiscreteGenerators

3import FoxDifferential.Completed.Continuous.Free.Rules

4import FoxDifferential.Completed.Continuous.Topology

5import FoxDifferential.Completed.Continuous.ChainRule.Basic

6import FoxDifferential.Completed.Continuous.ChainRule.Iterated

7import FoxDifferential.Common.Jacobian

8import FoxDifferential.Completed.Continuous.Naturality

9import FoxDifferential.Completed.Continuous.TailExactness

10import FoxDifferential.Completed.Continuous.TopologicalGeneration

11import FoxDifferential.Completed.Continuous.Universal.Basic

12import FoxDifferential.Completed.Continuous.Universal.FiniteStage

13import FoxDifferential.Completed.Continuous.Universal.NaturalTopology

14import FoxDifferential.Completed.Continuous.Universal.System

15import FoxDifferential.Completed.Continuous.SemidirectKernelBasis

17/-

18PUBLIC_PAGE_SNAPSHOT

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

20lean_source: lean4/FoxDifferential/Completed/Continuous.lean

21translation_root: data/translation

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

23placement: after imports, never before imports

24-/

25/-!

26# Continuous crossed differentials

28Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.

29-/