ProCGroups.FoxDifferential.Completed.Continuous.Free

5 sections | 5 files | 36 declarations

This aggregate re-exports the following parts of the Fox differential API:

Completed.Continuous.Free.DiscreteGenerators - Completed.Continuous.Free.Rules

imports

Imported by

ProCGroups.FoxDifferential.Completed.Continuous

CanonicalFormula

1 file | 3 declarations | 3 Theorems

The principal declarations in this module are: - `freeProCZCCompletedFoxDerivativeVector_boundary` Boundary-map form of the source-shaped completed Fox formula for the canonical...

Continuity

1 file | 15 declarations | 15 Theorems

The principal declarations in this module are: - `continuous_freeProCZCCompletedFoxSemidirectGenerator` The completed Fox semidirect generator map is continuous when both compon...

DiscreteGenerators

1 file | 4 declarations | 4 Theorems

The principal declarations in this module are: - `existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators` Continuous completed Fox semidirect homomorphisms f...

Rules

1 file | 13 declarations | 11 Theorems | 2 Definitions

The principal declarations in this module are: - `freeProCZCCompletedFoxRightHomContinuousMonoidHom` The right component of the completed free pro-\(C\) Fox lift is bundled as a...

SourceFormula

1 file | 1 declaration | 1 Theorem

The principal declarations in this module are: - `freeProCZCCompletedFoxBoundary_of_continuousCrossedDifferential` Source-shaped completed Fox boundary formula for continuous cr...