FoxDifferential/Completed/DifferentialModule.lean

1import FoxDifferential.Completed.DifferentialModule.Identity

2import FoxDifferential.Completed.DifferentialModule.Map.Comap

3import FoxDifferential.Completed.DifferentialModule.Map.GroupLike

4import FoxDifferential.Completed.DifferentialModule.Map.Limit

5import FoxDifferential.Completed.DifferentialModule.Map.Stage

6import FoxDifferential.Completed.DifferentialModule.Map.Surjective

7import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Basic

8import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental

9import FoxDifferential.Completed.DifferentialModule.TargetQuotient.MulProjection

10import FoxDifferential.Completed.DifferentialModule.TargetQuotient.StageMap

11import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Surjective

13/-

14PUBLIC_PAGE_SNAPSHOT

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

16lean_source: lean4/FoxDifferential/Completed/DifferentialModule.lean

17translation_root: data/translation

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

19placement: after imports, never before imports

20-/

21/-!

22# Completed differential modules

24The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.

25-/