Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.DifferentialModule
ProCGroups/FoxDifferential/Completed/DifferentialModule/Source

Source: ProCGroups.FoxDifferential.Completed.DifferentialModule

1import ProCGroups.FoxDifferential.Completed.DifferentialModule.Identity
2import ProCGroups.FoxDifferential.Completed.DifferentialModule.Map
3import ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient
5/-!
6# Fox differential: completed — differential module
8This aggregate re-exports the following parts of the Fox differential API:
10- `Completed.DifferentialModule.Identity`
11- `Completed.DifferentialModule.Map`
12- `Completed.DifferentialModule.TargetQuotient`
13-/