OAI/NumberTheory/OrdinaryCorrelations/HighTrace/DivisorPath.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPath line 20
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPath.spec line 27
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPath.expression line 28
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPath.extra_absent line 29
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPath.eval line 30
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPath.nonzero line 34
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPath.support_card line 41
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPath.numeric_holds line 49
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.shortCorrupted line 57
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.shortCorruptPath line 63
11. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection line 66
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.shortCorruptSelection_exists line 72