OAI/NumberTheory/OrdinaryCorrelations/HighTrace/WitnessTestShape.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTestShapeline 21 - def
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTestShape.equivline 33 - instance
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTestShape.(instance at line 40)line 40 - def
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTestShape.expressionline 45 - lemma
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTestShape.expression_relabelline 59 - lemma
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTestShape.cardline 67 - def
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.shapeline 78 - lemma
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.shape_expressionline 101 - lemma
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.pattern_shape_expressionline 118