Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.FreeProC
ProCGroups/FoxDifferential/Completed/FreeProC/Source

Source: ProCGroups.FoxDifferential.Completed.FreeProC

1import ProCGroups.FoxDifferential.Completed.FreeProC.BifilteredCoefficientStageProjection
2import ProCGroups.FoxDifferential.Completed.FreeProC.BifilteredStageProjection
3import ProCGroups.FoxDifferential.Completed.FreeProC.BifilteredSystemStageProjection
4import ProCGroups.FoxDifferential.Completed.FreeProC.CofinalQuotientKernelBasis
5import ProCGroups.FoxDifferential.Completed.FreeProC.CoordinateStageProjection
6import ProCGroups.FoxDifferential.Completed.FreeProC.Density
7import ProCGroups.FoxDifferential.Completed.FreeProC.FiniteQuotientStages
8import ProCGroups.FoxDifferential.Completed.FreeProC.PrimePowerStageProjection
9import ProCGroups.FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageProjection
10import ProCGroups.FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageRightProjection
11import ProCGroups.FoxDifferential.Completed.FreeProC.ProCIntegerStageCoeffProjection
12import ProCGroups.FoxDifferential.Completed.FreeProC.QuotientKernelBasis
13import ProCGroups.FoxDifferential.Completed.FreeProC.RelationSubmoduleApproximation
14import ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectKernelBasis
15import ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift
16import ProCGroups.FoxDifferential.Completed.FreeProC.StageApproximation
17import ProCGroups.FoxDifferential.Completed.FreeProC.StageProjection
18import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness
19import ProCGroups.FoxDifferential.Completed.FreeProC.RelationReflection
20import ProCGroups.FoxDifferential.Completed.FreeProC.NaturalTopology
21import ProCGroups.FoxDifferential.Completed.FreeProC.Coordinates
22import ProCGroups.FoxDifferential.Completed.FreeProC.FundamentalFormula
24/-!
25# Fox differential: completed — free pro-\(C\)
27This aggregate re-exports the following parts of the Fox differential API:
29- `Completed.FreeProC.BifilteredCoefficientStageProjection`
30- `Completed.FreeProC.BifilteredStageProjection`
31- `Completed.FreeProC.BifilteredSystemStageProjection`
32- `Completed.FreeProC.CofinalQuotientKernelBasis`
33- `Completed.FreeProC.CoordinateStageProjection`
34- `Completed.FreeProC.Density`
35- `Completed.FreeProC.FiniteQuotientStages`
36- `Completed.FreeProC.PrimePowerStageProjection`
37- `Completed.FreeProC.ProCIntegerBifilteredStageProjection`
38- `Completed.FreeProC.ProCIntegerBifilteredStageRightProjection`
39- `Completed.FreeProC.ProCIntegerStageCoeffProjection`
40- `Completed.FreeProC.QuotientKernelBasis`
41- `Completed.FreeProC.RelationSubmoduleApproximation`
42- `Completed.FreeProC.SemidirectKernelBasis`
43- `Completed.FreeProC.SemidirectLift`
44- `Completed.FreeProC.StageApproximation`
45- `Completed.FreeProC.StageProjection`
46- `Completed.FreeProC.Uniqueness`
47- `Completed.FreeProC.RelationReflection`
48- `Completed.FreeProC.NaturalTopology`
49- `Completed.FreeProC.Coordinates`
50- `Completed.FreeProC.FundamentalFormula`
51-/