ProCGroups.FoxDifferential.Completed.Continuous.Universal

5 sections | 5 files | 430 declarations

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

Completed.Continuous.Universal.AugmentationQuotient - Completed.Continuous.Universal.Basic - Completed.Continuous.Universal.FiniteStage - Completed.Continuous.Universal.NaturalTopology - Completed.Continuous.Universal.System

imports

Imported by

ProCGroups.FoxDifferential.Completed.Continuous

AugmentationQuotient

1 file | 203 declarations | 150 Theorems | 49 Definitions | 4 Abbreviations

The principal declarations in this module are: - `zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard` The algebraic product \(I(\ker \psi)I(G)\) inside the algebraic stan...

Basic

1 file | 30 declarations | 16 Theorems | 11 Definitions | 3 Instances

The principal declarations in this module are: - `zcUniversalDifferentialFinalTopology` The final topology on the completed universal differential module generated by the univer...

FiniteStage

The principal declarations in this module are: - `ZCCompletedDifferentialModuleIndex` A finite stage for the completed universal differential module. It consists of a finite sou...

NaturalTopology

1 file | 102 declarations | 76 Theorems | 23 Definitions | 3 Abbreviations

The principal declarations in this module are: - `zcCompletedDifferentialModuleStageProjectionAdd` The additive finite-stage projection from the algebraic completed differential...

System

The principal declarations in this module are: - `zcCompletedDifferentialModuleStageSystem` The inverse system of finite source, target, and coefficient stages of \(A_{\psi}(C)\...