Yamaguchi Lean 4 Library
FoxDifferential.Completed.FiniteStage.PrimePower
FoxDifferential/Completed/FiniteStage/PrimePower

FoxDifferential.Completed.FiniteStage.PrimePower

3 sections | 30 files | 164 declarations

Wrapper for the FoxDifferential.Completed.FiniteStage.PrimePower folder.

Completion

6 files | 28 declarations | 22 Theorem | 6 Definition
Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

Derivative

15 files | 54 declarations | 46 Theorem | 8 Definition
Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

System

9 files | 82 declarations | 41 Theorem | 14 Definition | 6 Abbreviation | 21 Instance
Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.