Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.Continuous.ChainRule
ProCGroups/FoxDifferential/Completed/Continuous/ChainRule

ProCGroups.FoxDifferential.Completed.Continuous.ChainRule

2 sections | 2 files | 29 declarations

This aggregate re-exports the following parts of the Fox differential API:

  • Completed.Continuous.ChainRule.Basic - Completed.Continuous.ChainRule.Iterated
imports
Imported by

Basic

1 file | 17 declarations | 12 Theorems | 5 Definitions
The principal declarations in this module are: - `allFinite_freeProCZCCompletedFoxPullbackGenerator` The target generator map pulled back along a continuous homomorphism of free...

Iterated

1 file | 12 declarations | 10 Theorems | 2 Abbreviations
The principal declarations in this module are: - `allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator` The pulled-back target generator on the middle free source in a two-st...