OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairReferenceSourceTransportBlocks.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.typedBlockEquiv line 24
  2. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.typedBlockEquiv_label line 27
  3. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.typedBlockEquiv_transport line 32
  4. abbrev OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.TypedSourceIndex line 40
  5. def OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.typedSourceEquiv line 42
  6. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.typedSourceEquiv_giant line 48
  7. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.typedSourceEquiv_root line 51
  8. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.typedSourceEquiv_block line 55
  9. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.typedSourceEquiv_transport line 59
  10. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.typedSourceEquiv_pullSample line 72