OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SegmentEdges.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.segmentEdgesline 19 - def
OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.segmentSupportline 22 - lemma
OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.mem_segmentSupport_iffline 25 - def
OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.segmentCoefficientline 36 - lemma
OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.segmentCoefficient_zeroline 41