OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Index.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.index line 30
  2. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData line 33
  3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.pathData_exists line 45
  4. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.OrderedSelection line 58
  5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.orderedSelection_exists line 61
  6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.rootOffset line 91
  7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.firstExpression line 92
  8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.secondExpression line 93
  9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.expression line 94
  10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.expression_eval line 96
  11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.expression_nonzero line 103
  12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.expression_divides line 113
  13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.expression_earlier line 121
  14. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.selected line 129
  15. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.tests line 130