ProCGroups.FoxDifferential.RightDerivative

2 sections | 2 files | 25 declarations

This compatibility-free root collects the geometric-series and semidirect-product constructions used by right Fox calculus. Right differentials themselves use the general CrossedHom API.

imports
Imported by

GeometricSeries

1 file | 11 declarations | 10 Theorems | 1 Definition
The principal declarations in this module are: - `geomSeries` The geometric series element is the finite sum of successive powers. - `geomSeries_eq_sum_pow` The geometric series...

Semidirect

1 file | 14 declarations | 8 Theorems | 1 Definition | 1 Structure | 4 Instances
The principal declarations in this module are: - `RightFoxSemidirect` The right Fox semidirect product records a group element together with its right-derivative coordinate. - `...