All.lean
Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.All
0 declarations indexed from sourceView source ↗
Module documentation
Fox differential: completed — free pro-\(C\) — uniqueness
This aggregate re-exports the following parts of the Fox differential API:
Completed.FreeProC.Uniqueness.DerivativeCompleted.FreeProC.Uniqueness.ExistenceCompleted.FreeProC.Uniqueness.LiftCompleted.FreeProC.Uniqueness.MorphismCompleted.FreeProC.Uniqueness.SemidirectHom
Imports5
- Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Derivative
- Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Existence
- Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Lift
- Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Morphism
- Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom
This module has no indexed declarations. Its imports and full source are available here.