OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairSourceCoordinatesDecoded.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryPairSourceCoordinates.blockSourceEquiv line 14
  2. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceCoordinates.blockSourceEquiv_giant line 21
  3. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceCoordinates.blockSourceEquiv_root line 26
  4. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceCoordinates.blockSourceEquiv_block line 32
  5. def OAI.Ostmann.Arithmetic.HistoryPairSourceCoordinates.decodedSourceEquiv line 49
  6. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceCoordinates.decodedSourceEquiv_block_sample line 57
  7. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceCoordinates.decodedSourceEquiv_root_sample line 65
  8. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceCoordinates.decodedSourceEquiv_giant_sample line 71
  9. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceCoordinates.decodedSourceEquiv_sample line 80