Yamaguchi Lean 4 Library
FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN

5 sections | 12 files | 121 declarations

Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.

Augmentation

1 files | 9 declarations | 6 Theorem | 3 Definition
The augmentation on one residue-coefficient finite stage.

AugmentationIdeal

1 files | 20 declarations | 10 Theorem | 7 Definition | 3 Abbreviation
The augmentation ideal on one residue-coefficient finite stage.

CoeffMap

1 files | 5 declarations | 3 Theorem | 2 Definition
Fox Differential / Completed / Coefficient Rings / Completed Group Algebra Mod N / Coefficient Map.

InClass

5 files | 50 declarations | 31 Theorem | 6 Definition | 5 Abbreviation | 8 Instance
Fox Differential / Completed / Coefficient Rings / Completed Group Algebra Mod N / Within a Class.

System

4 files | 37 declarations | 19 Theorem | 4 Definition | 3 Abbreviation | 11 Instance
Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.