OAI/NumberTheory/Ostmann/Arithmetic/IntegerHistoryReconstruction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The cleared formulas evaluate to the actual integer pivot reconstructions

  1. structure OAI.Ostmann.HistoryPivotStep line 12
  2. def OAI.Ostmann.HistoryPivotStep.formula line 25
  3. def OAI.Ostmann.HistoryPivotStep.numerator line 29
  4. def OAI.Ostmann.HistoryPivotStep.Valid line 32
  5. def OAI.Ostmann.HistoryPivotStep.applyInteger line 34
  6. theorem OAI.Ostmann.HistoryPivotStep.formula_value line 37
  7. theorem OAI.Ostmann.HistoryPivotStep.formula_value_integer line 47
  8. theorem OAI.Ostmann.HistoryPivotStep.applyInteger_cast line 51
  9. theorem OAI.Ostmann.HistoryPivotStep.formula_cost line 61
  10. def OAI.Ostmann.reconstructIntegers line 73
  11. def OAI.Ostmann.ValidIntegerReconstruction line 77
  12. def OAI.Ostmann.integerReconstructionFormulas line 81
  13. theorem OAI.Ostmann.replay_integer_history line 85
  14. theorem OAI.Ostmann.integerReconstructionFormulas_value line 95