Yamaguchi Lean 4 Library
FoxDifferential.Discrete
FoxDifferential/Discrete

FoxDifferential.Discrete

8 sections | 24 files | 324 declarations

This module formalizes the discrete Fox calculus.

Absolute

1 files | 11 declarations | 10 Theorem | 1 Definition
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

DifferentialModule

4 files | 49 declarations | 31 Theorem | 14 Definition | 4 Abbreviation
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

FoxCalculus

6 files | 44 declarations | 32 Theorem | 6 Definition | 1 Abbreviation | 1 Structure | 4 Instance
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

FreeExpansion

1 files | 7 declarations | 6 Theorem | 1 Definition
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

GroupRing

1 files | 28 declarations | 19 Theorem | 9 Definition
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Jacobian

4 files | 31 declarations | 26 Theorem | 5 Definition
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

KernelBoundary

6 files | 150 declarations | 87 Theorem | 50 Definition | 12 Abbreviation | 1 Instance
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Naturality

1 files | 4 declarations | 3 Theorem | 1 Definition
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.