ProCGroups.FoxDifferential.Completed.DifferentialModule

3 sections | 13 files | 44 declarations

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

Completed.DifferentialModule.Identity - Completed.DifferentialModule.Map - Completed.DifferentialModule.TargetQuotient

imports

Imported by

ProCGroups.FoxDifferential.Completed

Identity

1 file | 11 declarations | 5 Theorems | 6 Definitions

The principal declarations in this module are: - `identityCompletedGroupAlgebraOpenSubgroup` The identity completed-group-algebra open subgroup used for the identity quotient st...

Map

6 files | 20 declarations | 15 Theorems | 5 Definitions

This aggregate re-exports the following parts of the Fox differential API: - `Completed.DifferentialModule.Map.Comap` - `Completed.DifferentialModule.Map.GroupLike` - `Completed...

TargetQuotient

6 files | 13 declarations | 11 Theorems | 2 Definitions

This aggregate re-exports the following parts of the Fox differential API: - `Completed.DifferentialModule.TargetQuotient.Basic` - `Completed.DifferentialModule.TargetQuotient.F...