OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkPriorGridBasic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkLogLower line 17
  2. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkLogUpper line 18
  3. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkPrimeCutoff line 19
  4. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkClosedSupport line 20
  5. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkBoundary line 22
  6. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkRemoved line 24
  7. theorem OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.mem_bulkPrimeBand line 26
  8. theorem OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.mem_bulkClosedSupport line 44
  9. theorem OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkBoundary_card_le_one line 56
  10. theorem OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkRemoved_card_le line 68
  11. theorem OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkPrimeBand_eq_closed_sdiff line 72
  12. theorem OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkPrimeBand_subset_closed line 92