OAI/Analysis/Quantum/DimensionTen/Mod131Powers04.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Mod131.pow7_2 line 8
  2. def OAI.DimensionTen.Mod131.pow7_2_q line 10
  3. def OAI.DimensionTen.Mod131.pow7_2_mul_t line 12
  4. theorem OAI.DimensionTen.Mod131.pow7_2_mul_integer line 14
  5. theorem OAI.DimensionTen.Mod131.pow7_2_mul line 20
  6. theorem OAI.DimensionTen.Mod131.pow7_2_root line 26
  7. theorem OAI.DimensionTen.Mod131.pow7_2_pow line 31
  8. def OAI.DimensionTen.Mod131.pow7_4 line 39
  9. def OAI.DimensionTen.Mod131.pow7_4_q line 41
  10. def OAI.DimensionTen.Mod131.pow7_4_mul_t line 43
  11. theorem OAI.DimensionTen.Mod131.pow7_4_mul_integer line 45
  12. theorem OAI.DimensionTen.Mod131.pow7_4_mul line 51
  13. theorem OAI.DimensionTen.Mod131.pow7_4_root line 57
  14. theorem OAI.DimensionTen.Mod131.pow7_4_pow line 62
  15. def OAI.DimensionTen.Mod131.pow7_8 line 70
  16. def OAI.DimensionTen.Mod131.pow7_8_q line 72
  17. def OAI.DimensionTen.Mod131.pow7_8_mul_t line 74
  18. theorem OAI.DimensionTen.Mod131.pow7_8_mul_integer line 76
  19. theorem OAI.DimensionTen.Mod131.pow7_8_mul line 82
  20. theorem OAI.DimensionTen.Mod131.pow7_8_root line 88
  21. theorem OAI.DimensionTen.Mod131.pow7_8_pow line 93
  22. def OAI.DimensionTen.Mod131.pow7_16 line 101
  23. def OAI.DimensionTen.Mod131.pow7_16_q line 103
  24. def OAI.DimensionTen.Mod131.pow7_16_mul_t line 105
  25. theorem OAI.DimensionTen.Mod131.pow7_16_mul_integer line 107
  26. theorem OAI.DimensionTen.Mod131.pow7_16_mul line 113
  27. theorem OAI.DimensionTen.Mod131.pow7_16_root line 119
  28. theorem OAI.DimensionTen.Mod131.pow7_16_pow line 124
  29. def OAI.DimensionTen.Mod131.pow7_32 line 132
  30. def OAI.DimensionTen.Mod131.pow7_32_q line 134
  31. def OAI.DimensionTen.Mod131.pow7_32_mul_t line 136
  32. theorem OAI.DimensionTen.Mod131.pow7_32_mul_integer line 138
  33. theorem OAI.DimensionTen.Mod131.pow7_32_mul line 144
  34. theorem OAI.DimensionTen.Mod131.pow7_32_root line 150
  35. theorem OAI.DimensionTen.Mod131.pow7_32_pow line 155
  36. def OAI.DimensionTen.Mod131.pow7_64 line 163
  37. def OAI.DimensionTen.Mod131.pow7_64_q line 165
  38. def OAI.DimensionTen.Mod131.pow7_64_mul_t line 167
  39. theorem OAI.DimensionTen.Mod131.pow7_64_mul_integer line 169
  40. theorem OAI.DimensionTen.Mod131.pow7_64_mul line 175
  41. theorem OAI.DimensionTen.Mod131.pow7_64_root line 181
  42. theorem OAI.DimensionTen.Mod131.pow7_64_pow line 186
  43. def OAI.DimensionTen.Mod131.pow7_65 line 194
  44. def OAI.DimensionTen.Mod131.pow7_65_q line 196
  45. def OAI.DimensionTen.Mod131.pow7_65_mul_t line 198
  46. theorem OAI.DimensionTen.Mod131.pow7_65_mul_integer line 200
  47. theorem OAI.DimensionTen.Mod131.pow7_65_mul line 206
  48. theorem OAI.DimensionTen.Mod131.pow7_65_root line 212
  49. theorem OAI.DimensionTen.Mod131.pow7_65_pow line 217
  50. def OAI.DimensionTen.Mod131.pow7_130 line 223
  51. def OAI.DimensionTen.Mod131.pow7_130_q line 225
  52. def OAI.DimensionTen.Mod131.pow7_130_mul_t line 227
  53. theorem OAI.DimensionTen.Mod131.pow7_130_mul_integer line 229
  54. theorem OAI.DimensionTen.Mod131.pow7_130_mul line 235
  55. theorem OAI.DimensionTen.Mod131.pow7_130_root line 241
  56. theorem OAI.DimensionTen.Mod131.pow7_130_pow line 246
  57. def OAI.DimensionTen.Mod131.pow7_131 line 254
  58. def OAI.DimensionTen.Mod131.pow7_131_q line 256
  59. def OAI.DimensionTen.Mod131.pow7_131_mul_t line 258
  60. theorem OAI.DimensionTen.Mod131.pow7_131_mul_integer line 260
  61. theorem OAI.DimensionTen.Mod131.pow7_131_mul line 266
  62. theorem OAI.DimensionTen.Mod131.pow7_131_root line 272
  63. theorem OAI.DimensionTen.Mod131.pow7_131_pow line 277
  64. abbrev OAI.DimensionTen.Mod131.u7 line 283
  65. theorem OAI.DimensionTen.Mod131.iterate7 line 285
  66. def OAI.DimensionTen.Mod131.pow8_2 line 293
  67. def OAI.DimensionTen.Mod131.pow8_2_q line 295
  68. def OAI.DimensionTen.Mod131.pow8_2_mul_t line 297
  69. theorem OAI.DimensionTen.Mod131.pow8_2_mul_integer line 299
  70. theorem OAI.DimensionTen.Mod131.pow8_2_mul line 305
  71. theorem OAI.DimensionTen.Mod131.pow8_2_root line 311
  72. theorem OAI.DimensionTen.Mod131.pow8_2_pow line 316
  73. def OAI.DimensionTen.Mod131.pow8_4 line 324
  74. def OAI.DimensionTen.Mod131.pow8_4_q line 326
  75. def OAI.DimensionTen.Mod131.pow8_4_mul_t line 328
  76. theorem OAI.DimensionTen.Mod131.pow8_4_mul_integer line 330
  77. theorem OAI.DimensionTen.Mod131.pow8_4_mul line 336
  78. theorem OAI.DimensionTen.Mod131.pow8_4_root line 342
  79. theorem OAI.DimensionTen.Mod131.pow8_4_pow line 347
  80. def OAI.DimensionTen.Mod131.pow8_8 line 355
  81. def OAI.DimensionTen.Mod131.pow8_8_q line 357
  82. def OAI.DimensionTen.Mod131.pow8_8_mul_t line 359
  83. theorem OAI.DimensionTen.Mod131.pow8_8_mul_integer line 361
  84. theorem OAI.DimensionTen.Mod131.pow8_8_mul line 367
  85. theorem OAI.DimensionTen.Mod131.pow8_8_root line 373
  86. theorem OAI.DimensionTen.Mod131.pow8_8_pow line 378
  87. def OAI.DimensionTen.Mod131.pow8_16 line 386
  88. def OAI.DimensionTen.Mod131.pow8_16_q line 388
  89. def OAI.DimensionTen.Mod131.pow8_16_mul_t line 390
  90. theorem OAI.DimensionTen.Mod131.pow8_16_mul_integer line 392
  91. theorem OAI.DimensionTen.Mod131.pow8_16_mul line 398
  92. theorem OAI.DimensionTen.Mod131.pow8_16_root line 404
  93. theorem OAI.DimensionTen.Mod131.pow8_16_pow line 409
  94. def OAI.DimensionTen.Mod131.pow8_32 line 417
  95. def OAI.DimensionTen.Mod131.pow8_32_q line 419
  96. def OAI.DimensionTen.Mod131.pow8_32_mul_t line 421
  97. theorem OAI.DimensionTen.Mod131.pow8_32_mul_integer line 423
  98. theorem OAI.DimensionTen.Mod131.pow8_32_mul line 429
  99. theorem OAI.DimensionTen.Mod131.pow8_32_root line 435
  100. theorem OAI.DimensionTen.Mod131.pow8_32_pow line 440
  101. def OAI.DimensionTen.Mod131.pow8_64 line 448
  102. def OAI.DimensionTen.Mod131.pow8_64_q line 450
  103. def OAI.DimensionTen.Mod131.pow8_64_mul_t line 452
  104. theorem OAI.DimensionTen.Mod131.pow8_64_mul_integer line 454
  105. theorem OAI.DimensionTen.Mod131.pow8_64_mul line 460
  106. theorem OAI.DimensionTen.Mod131.pow8_64_root line 466
  107. theorem OAI.DimensionTen.Mod131.pow8_64_pow line 471
  108. def OAI.DimensionTen.Mod131.pow8_65 line 479
  109. def OAI.DimensionTen.Mod131.pow8_65_q line 481
  110. def OAI.DimensionTen.Mod131.pow8_65_mul_t line 483
  111. theorem OAI.DimensionTen.Mod131.pow8_65_mul_integer line 485
  112. theorem OAI.DimensionTen.Mod131.pow8_65_mul line 491
  113. theorem OAI.DimensionTen.Mod131.pow8_65_root line 497
  114. theorem OAI.DimensionTen.Mod131.pow8_65_pow line 502
  115. def OAI.DimensionTen.Mod131.pow8_130 line 508
  116. def OAI.DimensionTen.Mod131.pow8_130_q line 510
  117. def OAI.DimensionTen.Mod131.pow8_130_mul_t line 512
  118. theorem OAI.DimensionTen.Mod131.pow8_130_mul_integer line 514
  119. theorem OAI.DimensionTen.Mod131.pow8_130_mul line 520
  120. theorem OAI.DimensionTen.Mod131.pow8_130_root line 526
  121. theorem OAI.DimensionTen.Mod131.pow8_130_pow line 531
  122. def OAI.DimensionTen.Mod131.pow8_131 line 539
  123. def OAI.DimensionTen.Mod131.pow8_131_q line 541
  124. def OAI.DimensionTen.Mod131.pow8_131_mul_t line 543
  125. theorem OAI.DimensionTen.Mod131.pow8_131_mul_integer line 545
  126. theorem OAI.DimensionTen.Mod131.pow8_131_mul line 551
  127. theorem OAI.DimensionTen.Mod131.pow8_131_root line 557
  128. theorem OAI.DimensionTen.Mod131.pow8_131_pow line 562
  129. abbrev OAI.DimensionTen.Mod131.u8 line 568
  130. theorem OAI.DimensionTen.Mod131.iterate8 line 570