Yamaguchi Lean 4 Library
FoxDifferential.RightDerivative
FoxDifferential/RightDerivative

FoxDifferential.RightDerivative

5 sections | 5 files | 42 declarations

This module formalizes right Fox derivatives and their basic formulas.

Basic

1 files | 12 declarations | 8 Theorem | 2 Definition | 1 Structure | 1 Instance
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

CommutatorFormula

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

GeometricSeries

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.

IntegerPower

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

Semidirect

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