OAI/Analysis/Quantum/DimensionTen/Mod131Powers09.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Mod131.pow17_2 line 8
  2. def OAI.DimensionTen.Mod131.pow17_2_q line 10
  3. def OAI.DimensionTen.Mod131.pow17_2_mul_t line 12
  4. theorem OAI.DimensionTen.Mod131.pow17_2_mul_integer line 14
  5. theorem OAI.DimensionTen.Mod131.pow17_2_mul line 20
  6. theorem OAI.DimensionTen.Mod131.pow17_2_root line 26
  7. theorem OAI.DimensionTen.Mod131.pow17_2_pow line 31
  8. def OAI.DimensionTen.Mod131.pow17_4 line 39
  9. def OAI.DimensionTen.Mod131.pow17_4_q line 41
  10. def OAI.DimensionTen.Mod131.pow17_4_mul_t line 43
  11. theorem OAI.DimensionTen.Mod131.pow17_4_mul_integer line 45
  12. theorem OAI.DimensionTen.Mod131.pow17_4_mul line 51
  13. theorem OAI.DimensionTen.Mod131.pow17_4_root line 57
  14. theorem OAI.DimensionTen.Mod131.pow17_4_pow line 62
  15. def OAI.DimensionTen.Mod131.pow17_8 line 70
  16. def OAI.DimensionTen.Mod131.pow17_8_q line 72
  17. def OAI.DimensionTen.Mod131.pow17_8_mul_t line 74
  18. theorem OAI.DimensionTen.Mod131.pow17_8_mul_integer line 76
  19. theorem OAI.DimensionTen.Mod131.pow17_8_mul line 82
  20. theorem OAI.DimensionTen.Mod131.pow17_8_root line 88
  21. theorem OAI.DimensionTen.Mod131.pow17_8_pow line 93
  22. def OAI.DimensionTen.Mod131.pow17_16 line 101
  23. def OAI.DimensionTen.Mod131.pow17_16_q line 103
  24. def OAI.DimensionTen.Mod131.pow17_16_mul_t line 105
  25. theorem OAI.DimensionTen.Mod131.pow17_16_mul_integer line 107
  26. theorem OAI.DimensionTen.Mod131.pow17_16_mul line 113
  27. theorem OAI.DimensionTen.Mod131.pow17_16_root line 119
  28. theorem OAI.DimensionTen.Mod131.pow17_16_pow line 124
  29. def OAI.DimensionTen.Mod131.pow17_32 line 132
  30. def OAI.DimensionTen.Mod131.pow17_32_q line 134
  31. def OAI.DimensionTen.Mod131.pow17_32_mul_t line 136
  32. theorem OAI.DimensionTen.Mod131.pow17_32_mul_integer line 138
  33. theorem OAI.DimensionTen.Mod131.pow17_32_mul line 144
  34. theorem OAI.DimensionTen.Mod131.pow17_32_root line 150
  35. theorem OAI.DimensionTen.Mod131.pow17_32_pow line 155
  36. def OAI.DimensionTen.Mod131.pow17_64 line 163
  37. def OAI.DimensionTen.Mod131.pow17_64_q line 165
  38. def OAI.DimensionTen.Mod131.pow17_64_mul_t line 167
  39. theorem OAI.DimensionTen.Mod131.pow17_64_mul_integer line 169
  40. theorem OAI.DimensionTen.Mod131.pow17_64_mul line 175
  41. theorem OAI.DimensionTen.Mod131.pow17_64_root line 181
  42. theorem OAI.DimensionTen.Mod131.pow17_64_pow line 186
  43. def OAI.DimensionTen.Mod131.pow17_65 line 194
  44. def OAI.DimensionTen.Mod131.pow17_65_q line 196
  45. def OAI.DimensionTen.Mod131.pow17_65_mul_t line 198
  46. theorem OAI.DimensionTen.Mod131.pow17_65_mul_integer line 200
  47. theorem OAI.DimensionTen.Mod131.pow17_65_mul line 206
  48. theorem OAI.DimensionTen.Mod131.pow17_65_root line 212
  49. theorem OAI.DimensionTen.Mod131.pow17_65_pow line 217
  50. def OAI.DimensionTen.Mod131.pow17_130 line 223
  51. def OAI.DimensionTen.Mod131.pow17_130_q line 225
  52. def OAI.DimensionTen.Mod131.pow17_130_mul_t line 227
  53. theorem OAI.DimensionTen.Mod131.pow17_130_mul_integer line 229
  54. theorem OAI.DimensionTen.Mod131.pow17_130_mul line 235
  55. theorem OAI.DimensionTen.Mod131.pow17_130_root line 241
  56. theorem OAI.DimensionTen.Mod131.pow17_130_pow line 246
  57. def OAI.DimensionTen.Mod131.pow17_131 line 254
  58. def OAI.DimensionTen.Mod131.pow17_131_q line 256
  59. def OAI.DimensionTen.Mod131.pow17_131_mul_t line 258
  60. theorem OAI.DimensionTen.Mod131.pow17_131_mul_integer line 260
  61. theorem OAI.DimensionTen.Mod131.pow17_131_mul line 266
  62. theorem OAI.DimensionTen.Mod131.pow17_131_root line 272
  63. theorem OAI.DimensionTen.Mod131.pow17_131_pow line 277
  64. abbrev OAI.DimensionTen.Mod131.u17 line 283
  65. theorem OAI.DimensionTen.Mod131.iterate17 line 285