Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Residue.FreeGroup
ProCGroups/FoxDifferential/Completed/Residue/FreeGroup/Source

Source: ProCGroups.FoxDifferential.Completed.Residue.FreeGroup

1import ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Basic
2import ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Boundary
3import ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Coordinates
4import ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Fundamental
5import ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Universal
7/-!
8# Fox differential: completed — residue — free group
10This aggregate re-exports the following parts of the Fox differential API:
12- `Completed.Residue.FreeGroup.Basic`
13- `Completed.Residue.FreeGroup.Boundary`
14- `Completed.Residue.FreeGroup.Coordinates`
15- `Completed.Residue.FreeGroup.Fundamental`
16- `Completed.Residue.FreeGroup.Universal`
17-/