OAI/NumberTheory/Ostmann/Arithmetic/HistoryCompensationRepresentativePatternsDecoded.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.blockSourceDraws line 20
  2. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.blockLeftChoices line 23
  3. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.blockRightChoices line 26
  4. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.blockLeftHistory line 29
  5. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.blockRightHistory line 32
  6. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.blockLeftLabels line 40
  7. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.blockRightLabels line 44
  8. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.decoded_pair_slot_eq line 47
  9. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.decodedRepresentativeBlockEquiv line 70
  10. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.decodedRepresentativeBlockEquiv_prime line 79
  11. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.decodedRepresentativeBlockEquiv_multiplicity line 89
  12. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.decoded_unitKernel_product_le_blocks line 97
  13. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.decoded_mixedKernel_product_le_blocks line 108
  14. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.decoded_product_occurrences line 120