OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 48 imports below, so a file that imports it gets all of them.
Imports
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.ShapePivotBins
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.VertexIndex
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.FlatCode
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.UntaggedReferenceWeight
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.GeometryGoodEdges
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.ChargePivotAbsorption
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.SourceReturnFactor
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.IntegerResiduesAdd
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.ArithmeticSum
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.ForwardSegment
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.PrimeOccurrenceInterval
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.ReverseSegment
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.LastEdge
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.ExistsNewPrime
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.PrefixCoefficientNondvd
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.SourcePrimitiveCoefficientInputs
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.CoefficientZeroOfNotSupport
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.Precedes
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.SourceCylinderTruncation
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.SourceWitnessError
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.SupportEqUsed
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.LinePrimeCode
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.UnlitPolynomialBound
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.CoefficientEqSingle
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.PrimeIndex
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.GapFilling
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.PackedGapSum
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.PackedGapPrefactor
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.Edges
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.GapShapes
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.ForestCuts
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.Subpath
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.ActivityGapIndices
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.PostGapErrorSum
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.ComponentBoundAfterGap
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.DivisorPathFilling
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.PackedGapPrefactorMonoPath
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.DisconnectedErrorSum
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.AllForward
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.Expression
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.OrderedSelection
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.GateSelection
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.SelectedUsed
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.DisconnectedCertificate
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.WitnessBaseDoublePath
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.SourceDisconnectedCertificatesSmall
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.SourceFullTraceRaw
- OAI.NumberTheory.OrdinaryCorrelations.HighTrace.FullArithmeticTrace