FoxDifferential/Completed/Residue.lean

1import FoxDifferential.Completed.Residue.Core

2import FoxDifferential.Completed.Residue.FreeGroup.Basic

3import FoxDifferential.Completed.Residue.FreeGroup.Boundary

4import FoxDifferential.Completed.Residue.FreeGroup.Coordinates

5import FoxDifferential.Completed.Residue.FreeGroup.Fundamental

6import FoxDifferential.Completed.Residue.FreeGroup.Universal

8/-

9PUBLIC_PAGE_SNAPSHOT

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

11lean_source: lean4/FoxDifferential/Completed/Residue.lean

12translation_root: data/translation

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

14placement: after imports, never before imports

15-/

16/-!

17# Residue coefficient stages

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

20-/