OAI/NumberTheory/Ostmann/Arithmetic/HistorySymbolicSlots.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistorySymbolicSlots.Correct line 12
  2. def OAI.Ostmann.Arithmetic.HistorySymbolicSlots.reorder line 15
  3. theorem OAI.Ostmann.Arithmetic.HistorySymbolicSlots.correct_reorder line 18
  4. def OAI.Ostmann.Arithmetic.HistorySymbolicSlots.leftIndex line 25
  5. def OAI.Ostmann.Arithmetic.HistorySymbolicSlots.rightIndex line 28
  6. theorem OAI.Ostmann.Arithmetic.HistorySymbolicSlots.get_leftIndex line 31
  7. theorem OAI.Ostmann.Arithmetic.HistorySymbolicSlots.get_rightIndex line 35
  8. def OAI.Ostmann.Arithmetic.HistorySymbolicSlots.leftPart line 39
  9. def OAI.Ostmann.Arithmetic.HistorySymbolicSlots.rightPart line 42
  10. theorem OAI.Ostmann.Arithmetic.HistorySymbolicSlots.correct_leftPart line 45
  11. theorem OAI.Ostmann.Arithmetic.HistorySymbolicSlots.correct_rightPart line 51
  12. def OAI.Ostmann.Arithmetic.HistorySymbolicSlots.append line 57
  13. theorem OAI.Ostmann.Arithmetic.HistorySymbolicSlots.correct_append line 61
  14. theorem OAI.Ostmann.Arithmetic.HistorySymbolicSlots.product_correct line 74