OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkReferenceTestsBasic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.ownPrimeLineAt line 13
  2. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.ownPrimeSquareLineAt line 20
  3. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.finiteOwnPrimeLinesAt line 27
  4. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.primeResidueIndicatorAt line 33
  5. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.ownPrimeLineAt_intCast line 38
  6. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.ownPrimeSquareLineAt_intCast line 46
  7. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.finiteOwnPrimeLinesAt_intCast_iff line 54
  8. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.primeResidueIndicatorAt_ne_zero_iff line 66
  9. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.tests_of_primeResidueIndicatorAt_ne_zero line 73
  10. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.ownPrimeLineAt_pairSample line 84
  11. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.ownPrimeSquareLineAt_pairSample line 90
  12. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceTests.primeResidueIndicatorAt_pairSample line 96