ProCGroups.FoxDifferential.Completed.FiniteStage.Stage

6 sections | 16 files | 113 declarations

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

Completed.FiniteStage.Stage.Derivative - Completed.FiniteStage.Stage.Fundamental - Completed.FiniteStage.Stage.KernelIdeal - Completed.FiniteStage.Stage.Naturality - Completed.FiniteStage.Stage.Semidirect - Completed.FiniteStage.Stage.Source

imports

Imported by

ProCGroups.FoxDifferential.Completed.FiniteStage

Derivative

9 files | 53 declarations | 42 Theorems | 11 Definitions

This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.Stage.Derivative.Boundary` - `Completed.FiniteStage.Stage.Derivative.Quotient...

Fundamental

3 files | 9 declarations | 8 Theorems | 1 Definition

This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.Stage.Fundamental.Formula`

KernelIdeal

1 file | 2 declarations | 2 Theorems

The principal declarations in this module are: - `foxAlgebraicStageSourceGeneratorSubOne_mem_sourceAugmentationIdeal` The finite-stage source generator \([x_i]-1\) belongs to th...

Naturality

1 file | 18 declarations | 13 Theorems | 5 Definitions

The principal declarations in this module are: - `foxAlgebraicStageTargetQuotientMap` Natural quotient map \(F/N \to F/M\) induced by an inclusion \(N \le M\). - `foxAlgebraicSt...

Semidirect

The principal declarations in this module are: - `foxAlgebraicStageTargetQuotient` The finite-stage target quotient \(F/N\). - `foxAlgebraicStageTargetGroupAlgebra` The finite-s...

Source

1 file | 10 declarations | 7 Theorems | 3 Definitions

The principal declarations in this module are: - `foxAlgebraicStageSourceRepresentative` A chosen free-group representative of a finite Fox source quotient element, supplying so...