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

Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient

1import ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Basic
2import ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental
3import ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.MulProjection
4import ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.StageMap
5import ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Surjective
7/-!
8# Fox differential: completed — differential module — target quotient
10This aggregate re-exports the following parts of the Fox differential API:
12- `Completed.DifferentialModule.TargetQuotient.Basic`
13- `Completed.DifferentialModule.TargetQuotient.Fundamental`
14- `Completed.DifferentialModule.TargetQuotient.MulProjection`
15- `Completed.DifferentialModule.TargetQuotient.StageMap`
16- `Completed.DifferentialModule.TargetQuotient.Surjective`
17-/