OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairBulkCoordinatesBasic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.RootBulkPosition line 15
  2. def OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.rootKey line 18
  3. def OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.bulkCoordinates line 21
  4. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.root_value_injective line 24
  5. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.rootKey_injective line 42
  6. def OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.bulkEquiv line 49
  7. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.bulkEquiv_val line 59
  8. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.left_giant_not_mem line 62
  9. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.right_giant_not_mem line 69
  10. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.left_nonbulk_not_mem line 74
  11. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.left_internal_not_mem line 82
  12. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.right_internal_not_mem line 91