FoxDifferential/Completed/DifferentialModule/TargetQuotient.lean
1import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Basic
2import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental
3import FoxDifferential.Completed.DifferentialModule.TargetQuotient.MulProjection
4import FoxDifferential.Completed.DifferentialModule.TargetQuotient.StageMap
5import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Surjective
7/-
8PUBLIC_PAGE_SNAPSHOT
9generated_at: 2026-05-27T09:47:29+09:00
10lean_source: lean4/FoxDifferential/Completed/DifferentialModule/TargetQuotient.lean
11translation_root: data/translation
12purpose: identifies the local data snapshot used to build pages/
13placement: after imports, never before imports
14-/
15/-!
16# Completed differential modules
18The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
19-/