Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness
ProCGroups/FoxDifferential/Completed/FreeProC/Uniqueness/Source

Source: ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness

1import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Derivative
2import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Existence
3import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Lift
4import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Morphism
5import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom
7/-!
8# Fox differential: completed — free pro-\(C\) — uniqueness
10This aggregate re-exports the following parts of the Fox differential API:
12- `Completed.FreeProC.Uniqueness.Derivative`
13- `Completed.FreeProC.Uniqueness.Existence`
14- `Completed.FreeProC.Uniqueness.Lift`
15- `Completed.FreeProC.Uniqueness.Morphism`
16- `Completed.FreeProC.Uniqueness.SemidirectHom`
17-/