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

Source: ProCGroups.FoxDifferential.Completed.FiniteStage

1import ProCGroups.FoxDifferential.Completed.FiniteStage.Basic
2import ProCGroups.FoxDifferential.Completed.FiniteStage.Bifiltered
3import ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycleHom
4import ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycles
5import ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryQuotient
6import ProCGroups.FoxDifferential.Completed.FiniteStage.BoundarySubgroups
7import ProCGroups.FoxDifferential.Completed.FiniteStage.CoeffMap
8import ProCGroups.FoxDifferential.Completed.FiniteStage.MagnusQuotient
9import ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower
10import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationAction
11import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdeal
12import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdealDerivative
13import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdealPrimitive
14import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationModule
15import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationRealization
16import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationSubmodule
17import ProCGroups.FoxDifferential.Completed.FiniteStage.SemidirectCycles
18import ProCGroups.FoxDifferential.Completed.FiniteStage.SourceBoundary
19import ProCGroups.FoxDifferential.Completed.FiniteStage.SourceCycleReduction
20import ProCGroups.FoxDifferential.Completed.FiniteStage.SourceDerivativeVector
21import ProCGroups.FoxDifferential.Completed.FiniteStage.Stage
22import ProCGroups.FoxDifferential.Completed.FiniteStage.TargetMap
23import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationReflection
24import ProCGroups.FoxDifferential.Completed.FiniteStage.ClosedGeneratedCycles
26/-!
27# Fox differential: completed — finite stage
29This aggregate re-exports the following parts of the Fox differential API:
31- `Completed.FiniteStage.Basic`
32- `Completed.FiniteStage.Bifiltered`
33- `Completed.FiniteStage.BoundaryCycleHom`
34- `Completed.FiniteStage.BoundaryCycles`
35- `Completed.FiniteStage.BoundaryQuotient`
36- `Completed.FiniteStage.BoundarySubgroups`
37- `Completed.FiniteStage.CoeffMap`
38- `Completed.FiniteStage.MagnusQuotient`
39- `Completed.FiniteStage.PrimePower`
40- `Completed.FiniteStage.RelationAction`
41- `Completed.FiniteStage.RelationIdeal`
42- `Completed.FiniteStage.RelationIdealDerivative`
43- `Completed.FiniteStage.RelationIdealPrimitive`
44- `Completed.FiniteStage.RelationModule`
45- `Completed.FiniteStage.RelationRealization`
46- `Completed.FiniteStage.RelationSubmodule`
47- `Completed.FiniteStage.SemidirectCycles`
48- `Completed.FiniteStage.SourceBoundary`
49- `Completed.FiniteStage.SourceCycleReduction`
50- `Completed.FiniteStage.SourceDerivativeVector`
51- `Completed.FiniteStage.Stage`
52- `Completed.FiniteStage.TargetMap`
53- `Completed.FiniteStage.RelationReflection`
54- `Completed.FiniteStage.ClosedGeneratedCycles`
55-/