Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower
ProCGroups/FoxDifferential/Completed/FiniteStage/PrimePower

ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower

3 sections | 30 files | 162 declarations

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

  • Completed.FiniteStage.PrimePower.Completion - Completed.FiniteStage.PrimePower.Derivative - Completed.FiniteStage.PrimePower.System
imports
Imported by

Completion

6 files | 28 declarations | 22 Theorems | 6 Definitions
This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.PrimePower.Completion.Source` - `Completed.FiniteStage.PrimePower.Completion....

Derivative

15 files | 52 declarations | 44 Theorems | 8 Definitions
This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.PrimePower.Derivative.CompletedSource` - `Completed.FiniteStage.PrimePower.De...

System

9 files | 82 declarations | 41 Theorems | 14 Definitions | 6 Abbreviations | 21 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.PrimePower.System.Basic` - `Completed.FiniteStage.PrimePower.System.Limit` - ...