OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairBulkCoordinatesOrder.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.matchedRootPosition line 12
  2. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.matchedRootPosition_role line 16
  3. def OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.matchedBulkPositions line 21
  4. def OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.orderedEquiv line 27
  5. def OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.orderedKey line 33
  6. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.orderedEquiv_val line 38
  7. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.orderedKey_injective line 42
  8. def OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.insertOrdered line 48
  9. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.insertOrdered_left line 54
  10. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.matchedRootPosition_value line 63