OAI/Analysis/Quantum/DimensionTen/Mod139Powers05.lean

GitHub source file

144 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Mod139.pow9_2 line 8
  2. def OAI.DimensionTen.Mod139.pow9_2_q line 10
  3. def OAI.DimensionTen.Mod139.pow9_2_mul_t line 12
  4. theorem OAI.DimensionTen.Mod139.pow9_2_mul_integer line 14
  5. theorem OAI.DimensionTen.Mod139.pow9_2_mul line 20
  6. theorem OAI.DimensionTen.Mod139.pow9_2_root line 26
  7. theorem OAI.DimensionTen.Mod139.pow9_2_pow line 31
  8. def OAI.DimensionTen.Mod139.pow9_4 line 39
  9. def OAI.DimensionTen.Mod139.pow9_4_q line 41
  10. def OAI.DimensionTen.Mod139.pow9_4_mul_t line 43
  11. theorem OAI.DimensionTen.Mod139.pow9_4_mul_integer line 45
  12. theorem OAI.DimensionTen.Mod139.pow9_4_mul line 51
  13. theorem OAI.DimensionTen.Mod139.pow9_4_root line 57
  14. theorem OAI.DimensionTen.Mod139.pow9_4_pow line 62
  15. def OAI.DimensionTen.Mod139.pow9_8 line 70
  16. def OAI.DimensionTen.Mod139.pow9_8_q line 72
  17. def OAI.DimensionTen.Mod139.pow9_8_mul_t line 74
  18. theorem OAI.DimensionTen.Mod139.pow9_8_mul_integer line 76
  19. theorem OAI.DimensionTen.Mod139.pow9_8_mul line 82
  20. theorem OAI.DimensionTen.Mod139.pow9_8_root line 88
  21. theorem OAI.DimensionTen.Mod139.pow9_8_pow line 93
  22. def OAI.DimensionTen.Mod139.pow9_16 line 101
  23. def OAI.DimensionTen.Mod139.pow9_16_q line 103
  24. def OAI.DimensionTen.Mod139.pow9_16_mul_t line 105
  25. theorem OAI.DimensionTen.Mod139.pow9_16_mul_integer line 107
  26. theorem OAI.DimensionTen.Mod139.pow9_16_mul line 113
  27. theorem OAI.DimensionTen.Mod139.pow9_16_root line 119
  28. theorem OAI.DimensionTen.Mod139.pow9_16_pow line 124
  29. def OAI.DimensionTen.Mod139.pow9_17 line 132
  30. def OAI.DimensionTen.Mod139.pow9_17_q line 134
  31. def OAI.DimensionTen.Mod139.pow9_17_mul_t line 136
  32. theorem OAI.DimensionTen.Mod139.pow9_17_mul_integer line 138
  33. theorem OAI.DimensionTen.Mod139.pow9_17_mul line 144
  34. theorem OAI.DimensionTen.Mod139.pow9_17_root line 150
  35. theorem OAI.DimensionTen.Mod139.pow9_17_pow line 155
  36. def OAI.DimensionTen.Mod139.pow9_34 line 161
  37. def OAI.DimensionTen.Mod139.pow9_34_q line 163
  38. def OAI.DimensionTen.Mod139.pow9_34_mul_t line 165
  39. theorem OAI.DimensionTen.Mod139.pow9_34_mul_integer line 167
  40. theorem OAI.DimensionTen.Mod139.pow9_34_mul line 173
  41. theorem OAI.DimensionTen.Mod139.pow9_34_root line 179
  42. theorem OAI.DimensionTen.Mod139.pow9_34_pow line 184
  43. def OAI.DimensionTen.Mod139.pow9_68 line 192
  44. def OAI.DimensionTen.Mod139.pow9_68_q line 194
  45. def OAI.DimensionTen.Mod139.pow9_68_mul_t line 196
  46. theorem OAI.DimensionTen.Mod139.pow9_68_mul_integer line 198
  47. theorem OAI.DimensionTen.Mod139.pow9_68_mul line 204
  48. theorem OAI.DimensionTen.Mod139.pow9_68_root line 210
  49. theorem OAI.DimensionTen.Mod139.pow9_68_pow line 215
  50. def OAI.DimensionTen.Mod139.pow9_69 line 223
  51. def OAI.DimensionTen.Mod139.pow9_69_q line 225
  52. def OAI.DimensionTen.Mod139.pow9_69_mul_t line 227
  53. theorem OAI.DimensionTen.Mod139.pow9_69_mul_integer line 229
  54. theorem OAI.DimensionTen.Mod139.pow9_69_mul line 235
  55. theorem OAI.DimensionTen.Mod139.pow9_69_root line 241
  56. theorem OAI.DimensionTen.Mod139.pow9_69_pow line 246
  57. def OAI.DimensionTen.Mod139.pow9_138 line 252
  58. def OAI.DimensionTen.Mod139.pow9_138_q line 254
  59. def OAI.DimensionTen.Mod139.pow9_138_mul_t line 256
  60. theorem OAI.DimensionTen.Mod139.pow9_138_mul_integer line 258
  61. theorem OAI.DimensionTen.Mod139.pow9_138_mul line 264
  62. theorem OAI.DimensionTen.Mod139.pow9_138_root line 270
  63. theorem OAI.DimensionTen.Mod139.pow9_138_pow line 275
  64. def OAI.DimensionTen.Mod139.pow9_139 line 283
  65. def OAI.DimensionTen.Mod139.pow9_139_q line 285
  66. def OAI.DimensionTen.Mod139.pow9_139_mul_t line 287
  67. theorem OAI.DimensionTen.Mod139.pow9_139_mul_integer line 289
  68. theorem OAI.DimensionTen.Mod139.pow9_139_mul line 295
  69. theorem OAI.DimensionTen.Mod139.pow9_139_root line 301
  70. theorem OAI.DimensionTen.Mod139.pow9_139_pow line 306
  71. abbrev OAI.DimensionTen.Mod139.u9 line 312
  72. theorem OAI.DimensionTen.Mod139.iterate9 line 314
  73. def OAI.DimensionTen.Mod139.pow10_2 line 322
  74. def OAI.DimensionTen.Mod139.pow10_2_q line 324
  75. def OAI.DimensionTen.Mod139.pow10_2_mul_t line 326
  76. theorem OAI.DimensionTen.Mod139.pow10_2_mul_integer line 328
  77. theorem OAI.DimensionTen.Mod139.pow10_2_mul line 334
  78. theorem OAI.DimensionTen.Mod139.pow10_2_root line 340
  79. theorem OAI.DimensionTen.Mod139.pow10_2_pow line 345
  80. def OAI.DimensionTen.Mod139.pow10_4 line 353
  81. def OAI.DimensionTen.Mod139.pow10_4_q line 355
  82. def OAI.DimensionTen.Mod139.pow10_4_mul_t line 357
  83. theorem OAI.DimensionTen.Mod139.pow10_4_mul_integer line 359
  84. theorem OAI.DimensionTen.Mod139.pow10_4_mul line 365
  85. theorem OAI.DimensionTen.Mod139.pow10_4_root line 371
  86. theorem OAI.DimensionTen.Mod139.pow10_4_pow line 376
  87. def OAI.DimensionTen.Mod139.pow10_8 line 384
  88. def OAI.DimensionTen.Mod139.pow10_8_q line 386
  89. def OAI.DimensionTen.Mod139.pow10_8_mul_t line 388
  90. theorem OAI.DimensionTen.Mod139.pow10_8_mul_integer line 390
  91. theorem OAI.DimensionTen.Mod139.pow10_8_mul line 396
  92. theorem OAI.DimensionTen.Mod139.pow10_8_root line 402
  93. theorem OAI.DimensionTen.Mod139.pow10_8_pow line 407
  94. def OAI.DimensionTen.Mod139.pow10_16 line 415
  95. def OAI.DimensionTen.Mod139.pow10_16_q line 417
  96. def OAI.DimensionTen.Mod139.pow10_16_mul_t line 419
  97. theorem OAI.DimensionTen.Mod139.pow10_16_mul_integer line 421
  98. theorem OAI.DimensionTen.Mod139.pow10_16_mul line 427
  99. theorem OAI.DimensionTen.Mod139.pow10_16_root line 433
  100. theorem OAI.DimensionTen.Mod139.pow10_16_pow line 438
  101. def OAI.DimensionTen.Mod139.pow10_17 line 446
  102. def OAI.DimensionTen.Mod139.pow10_17_q line 448
  103. def OAI.DimensionTen.Mod139.pow10_17_mul_t line 450
  104. theorem OAI.DimensionTen.Mod139.pow10_17_mul_integer line 452
  105. theorem OAI.DimensionTen.Mod139.pow10_17_mul line 458
  106. theorem OAI.DimensionTen.Mod139.pow10_17_root line 464
  107. theorem OAI.DimensionTen.Mod139.pow10_17_pow line 469
  108. def OAI.DimensionTen.Mod139.pow10_34 line 475
  109. def OAI.DimensionTen.Mod139.pow10_34_q line 477
  110. def OAI.DimensionTen.Mod139.pow10_34_mul_t line 479
  111. theorem OAI.DimensionTen.Mod139.pow10_34_mul_integer line 481
  112. theorem OAI.DimensionTen.Mod139.pow10_34_mul line 487
  113. theorem OAI.DimensionTen.Mod139.pow10_34_root line 493
  114. theorem OAI.DimensionTen.Mod139.pow10_34_pow line 498
  115. def OAI.DimensionTen.Mod139.pow10_68 line 506
  116. def OAI.DimensionTen.Mod139.pow10_68_q line 508
  117. def OAI.DimensionTen.Mod139.pow10_68_mul_t line 510
  118. theorem OAI.DimensionTen.Mod139.pow10_68_mul_integer line 512
  119. theorem OAI.DimensionTen.Mod139.pow10_68_mul line 518
  120. theorem OAI.DimensionTen.Mod139.pow10_68_root line 524
  121. theorem OAI.DimensionTen.Mod139.pow10_68_pow line 529
  122. def OAI.DimensionTen.Mod139.pow10_69 line 537
  123. def OAI.DimensionTen.Mod139.pow10_69_q line 539
  124. def OAI.DimensionTen.Mod139.pow10_69_mul_t line 541
  125. theorem OAI.DimensionTen.Mod139.pow10_69_mul_integer line 543
  126. theorem OAI.DimensionTen.Mod139.pow10_69_mul line 549
  127. theorem OAI.DimensionTen.Mod139.pow10_69_root line 555
  128. theorem OAI.DimensionTen.Mod139.pow10_69_pow line 560
  129. def OAI.DimensionTen.Mod139.pow10_138 line 566
  130. def OAI.DimensionTen.Mod139.pow10_138_q line 568
  131. def OAI.DimensionTen.Mod139.pow10_138_mul_t line 570
  132. theorem OAI.DimensionTen.Mod139.pow10_138_mul_integer line 572
  133. theorem OAI.DimensionTen.Mod139.pow10_138_mul line 578
  134. theorem OAI.DimensionTen.Mod139.pow10_138_root line 584
  135. theorem OAI.DimensionTen.Mod139.pow10_138_pow line 589
  136. def OAI.DimensionTen.Mod139.pow10_139 line 597
  137. def OAI.DimensionTen.Mod139.pow10_139_q line 599
  138. def OAI.DimensionTen.Mod139.pow10_139_mul_t line 601
  139. theorem OAI.DimensionTen.Mod139.pow10_139_mul_integer line 603
  140. theorem OAI.DimensionTen.Mod139.pow10_139_mul line 609
  141. theorem OAI.DimensionTen.Mod139.pow10_139_root line 615
  142. theorem OAI.DimensionTen.Mod139.pow10_139_pow line 620
  143. abbrev OAI.DimensionTen.Mod139.u10 line 626
  144. theorem OAI.DimensionTen.Mod139.iterate10 line 628