OAI/NumberTheory/SingleFold/Packed.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleFold.Packed.digit line 7
  2. def OAI.SingleFold.Packed.pack line 9
  3. def OAI.SingleFold.Packed.Bits line 11
  4. lemma OAI.SingleFold.Packed.bits_testBit line 12
  5. lemma OAI.SingleFold.Packed.testBit_digit line 26
  6. lemma OAI.SingleFold.Packed.bits_blocks line 33
  7. lemma OAI.SingleFold.Packed.digit_lt line 43
  8. lemma OAI.SingleFold.Packed.digit_zero line 44
  9. lemma OAI.SingleFold.Packed.digit_of_lt line 45
  10. lemma OAI.SingleFold.Packed.digit_high line 46
  11. lemma OAI.SingleFold.Packed.pack_succ line 48
  12. lemma OAI.SingleFold.Packed.pack_cons line 50
  13. lemma OAI.SingleFold.Packed.pack_zero line 56
  14. lemma OAI.SingleFold.Packed.pack_add line 57
  15. lemma OAI.SingleFold.Packed.pack_mul line 59
  16. lemma OAI.SingleFold.Packed.pack_lt line 61
  17. lemma OAI.SingleFold.Packed.digit_pack line 70
  18. lemma OAI.SingleFold.Packed.pack_digits line 83
  19. lemma OAI.SingleFold.Packed.digits_ext line 98
  20. lemma OAI.SingleFold.Packed.bits_and line 105
  21. lemma OAI.SingleFold.Packed.bits_le line 116
  22. lemma OAI.SingleFold.Packed.bits_refl line 119
  23. lemma OAI.SingleFold.Packed.bits_zero_left line 120
  24. lemma OAI.SingleFold.Packed.bits_zero_right line 121
  25. lemma OAI.SingleFold.Packed.bits_one line 123
  26. lemma OAI.SingleFold.Packed.bits_full line 130
  27. def OAI.SingleFold.Packed.ones line 140
  28. lemma OAI.SingleFold.Packed.ones_mul line 141
  29. lemma OAI.SingleFold.Packed.geometric line 143
  30. lemma OAI.SingleFold.Packed.bits_mask line 153
  31. lemma OAI.SingleFold.Packed.bits_ones line 173
  32. lemma OAI.SingleFold.Packed.pack_sum line 177
  33. lemma OAI.SingleFold.Packed.digit_sum line 181
  34. lemma OAI.SingleFold.Packed.pack_injective line 191
  35. lemma OAI.SingleFold.Packed.unique_scale line 198
  36. lemma OAI.SingleFold.Packed.bits_trans line 216
  37. lemma OAI.SingleFold.Packed.pack_congr line 218
  38. lemma OAI.SingleFold.Packed.pack_const_zero line 222
  39. lemma OAI.SingleFold.Packed.pack_shift line 223
  40. lemma OAI.SingleFold.Packed.pack_init line 227
  41. lemma OAI.SingleFold.Packed.pack_last line 231
  42. lemma OAI.SingleFold.Packed.division_last line 234
  43. lemma OAI.SingleFold.Packed.update_coefficients line 245
  44. lemma OAI.SingleFold.Packed.update_identity line 278