Yamaguchi Lean 4 Library
FoxDifferential
FoxDifferential

FoxDifferential

4 sections | 256 files | 2884 declarations

This module formalizes Fox differentials and Fox coordinates for free and profinite groups.

Common

7 files | 136 declarations | 102 Theorem | 27 Definition | 2 Abbreviation | 1 Structure | 4 Instance
This module provides the common Fox differential definitions and identities.

Completed

218 files | 2382 declarations | 1673 Theorem | 446 Definition | 76 Abbreviation | 4 Structure | 183 Instance
This module formalizes completed Fox coordinates for profinite groups.

Discrete

25 files | 324 declarations | 214 Theorem | 87 Definition | 17 Abbreviation | 1 Structure | 5 Instance
This module formalizes the discrete Fox calculus.

RightDerivative

6 files | 42 declarations | 29 Theorem | 6 Definition | 2 Structure | 5 Instance
This module formalizes right Fox derivatives and their basic formulas.