OAI/NumberTheory/SingleFold/Binary.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleFold.Binary.Bits line 7
  2. lemma OAI.SingleFold.Binary.split line 9
  3. lemma OAI.SingleFold.Binary.zero_right line 19
  4. lemma OAI.SingleFold.Binary.choose_odd_iff line 32
  5. lemma OAI.SingleFold.Binary.le line 47
  6. lemma OAI.SingleFold.Binary.ofDigits_digit line 53
  7. lemma OAI.SingleFold.Binary.ofDigits_map_range line 66
  8. lemma OAI.SingleFold.Binary.choose_digit line 74
  9. def OAI.SingleFold.Binary.System line 89
  10. lemma OAI.SingleFold.Binary.extract_unique line 94
  11. lemma OAI.SingleFold.Binary.sound line 108
  12. lemma OAI.SingleFold.Binary.unique line 117
  13. lemma OAI.SingleFold.Binary.complete line 132
  14. lemma OAI.SingleFold.Compiler.MapSF.vector line 152
  15. lemma OAI.SingleFold.Compiler.ScalarSF.powerRel line 159
  16. lemma OAI.SingleFold.Binary.system_sf line 167
  17. theorem OAI.SingleFold.Binary.bits line 192