OAI/Analysis/Quantum/DimensionTen/Mod41Powers04.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Mod41.pow7_2 line 8
  2. def OAI.DimensionTen.Mod41.pow7_2_q line 10
  3. def OAI.DimensionTen.Mod41.pow7_2_mul_t line 12
  4. theorem OAI.DimensionTen.Mod41.pow7_2_mul_integer line 14
  5. theorem OAI.DimensionTen.Mod41.pow7_2_mul line 20
  6. theorem OAI.DimensionTen.Mod41.pow7_2_root line 26
  7. theorem OAI.DimensionTen.Mod41.pow7_2_pow line 31
  8. def OAI.DimensionTen.Mod41.pow7_4 line 39
  9. def OAI.DimensionTen.Mod41.pow7_4_q line 41
  10. def OAI.DimensionTen.Mod41.pow7_4_mul_t line 43
  11. theorem OAI.DimensionTen.Mod41.pow7_4_mul_integer line 45
  12. theorem OAI.DimensionTen.Mod41.pow7_4_mul line 51
  13. theorem OAI.DimensionTen.Mod41.pow7_4_root line 57
  14. theorem OAI.DimensionTen.Mod41.pow7_4_pow line 62
  15. def OAI.DimensionTen.Mod41.pow7_5 line 70
  16. def OAI.DimensionTen.Mod41.pow7_5_q line 72
  17. def OAI.DimensionTen.Mod41.pow7_5_mul_t line 74
  18. theorem OAI.DimensionTen.Mod41.pow7_5_mul_integer line 76
  19. theorem OAI.DimensionTen.Mod41.pow7_5_mul line 82
  20. theorem OAI.DimensionTen.Mod41.pow7_5_root line 88
  21. theorem OAI.DimensionTen.Mod41.pow7_5_pow line 93
  22. def OAI.DimensionTen.Mod41.pow7_10 line 99
  23. def OAI.DimensionTen.Mod41.pow7_10_q line 101
  24. def OAI.DimensionTen.Mod41.pow7_10_mul_t line 103
  25. theorem OAI.DimensionTen.Mod41.pow7_10_mul_integer line 105
  26. theorem OAI.DimensionTen.Mod41.pow7_10_mul line 111
  27. theorem OAI.DimensionTen.Mod41.pow7_10_root line 117
  28. theorem OAI.DimensionTen.Mod41.pow7_10_pow line 122
  29. def OAI.DimensionTen.Mod41.pow7_20 line 130
  30. def OAI.DimensionTen.Mod41.pow7_20_q line 132
  31. def OAI.DimensionTen.Mod41.pow7_20_mul_t line 134
  32. theorem OAI.DimensionTen.Mod41.pow7_20_mul_integer line 136
  33. theorem OAI.DimensionTen.Mod41.pow7_20_mul line 142
  34. theorem OAI.DimensionTen.Mod41.pow7_20_root line 148
  35. theorem OAI.DimensionTen.Mod41.pow7_20_pow line 153
  36. def OAI.DimensionTen.Mod41.pow7_40 line 161
  37. def OAI.DimensionTen.Mod41.pow7_40_q line 163
  38. def OAI.DimensionTen.Mod41.pow7_40_mul_t line 165
  39. theorem OAI.DimensionTen.Mod41.pow7_40_mul_integer line 167
  40. theorem OAI.DimensionTen.Mod41.pow7_40_mul line 173
  41. theorem OAI.DimensionTen.Mod41.pow7_40_root line 179
  42. theorem OAI.DimensionTen.Mod41.pow7_40_pow line 184
  43. def OAI.DimensionTen.Mod41.pow7_41 line 192
  44. def OAI.DimensionTen.Mod41.pow7_41_q line 194
  45. def OAI.DimensionTen.Mod41.pow7_41_mul_t line 196
  46. theorem OAI.DimensionTen.Mod41.pow7_41_mul_integer line 198
  47. theorem OAI.DimensionTen.Mod41.pow7_41_mul line 204
  48. theorem OAI.DimensionTen.Mod41.pow7_41_root line 210
  49. theorem OAI.DimensionTen.Mod41.pow7_41_pow line 215
  50. abbrev OAI.DimensionTen.Mod41.u7 line 221
  51. theorem OAI.DimensionTen.Mod41.iterate7 line 223
  52. def OAI.DimensionTen.Mod41.pow8_2 line 231
  53. def OAI.DimensionTen.Mod41.pow8_2_q line 233
  54. def OAI.DimensionTen.Mod41.pow8_2_mul_t line 235
  55. theorem OAI.DimensionTen.Mod41.pow8_2_mul_integer line 237
  56. theorem OAI.DimensionTen.Mod41.pow8_2_mul line 243
  57. theorem OAI.DimensionTen.Mod41.pow8_2_root line 249
  58. theorem OAI.DimensionTen.Mod41.pow8_2_pow line 254
  59. def OAI.DimensionTen.Mod41.pow8_4 line 262
  60. def OAI.DimensionTen.Mod41.pow8_4_q line 264
  61. def OAI.DimensionTen.Mod41.pow8_4_mul_t line 266
  62. theorem OAI.DimensionTen.Mod41.pow8_4_mul_integer line 268
  63. theorem OAI.DimensionTen.Mod41.pow8_4_mul line 274
  64. theorem OAI.DimensionTen.Mod41.pow8_4_root line 280
  65. theorem OAI.DimensionTen.Mod41.pow8_4_pow line 285
  66. def OAI.DimensionTen.Mod41.pow8_5 line 293
  67. def OAI.DimensionTen.Mod41.pow8_5_q line 295
  68. def OAI.DimensionTen.Mod41.pow8_5_mul_t line 297
  69. theorem OAI.DimensionTen.Mod41.pow8_5_mul_integer line 299
  70. theorem OAI.DimensionTen.Mod41.pow8_5_mul line 305
  71. theorem OAI.DimensionTen.Mod41.pow8_5_root line 311
  72. theorem OAI.DimensionTen.Mod41.pow8_5_pow line 316
  73. def OAI.DimensionTen.Mod41.pow8_10 line 322
  74. def OAI.DimensionTen.Mod41.pow8_10_q line 324
  75. def OAI.DimensionTen.Mod41.pow8_10_mul_t line 326
  76. theorem OAI.DimensionTen.Mod41.pow8_10_mul_integer line 328
  77. theorem OAI.DimensionTen.Mod41.pow8_10_mul line 334
  78. theorem OAI.DimensionTen.Mod41.pow8_10_root line 340
  79. theorem OAI.DimensionTen.Mod41.pow8_10_pow line 345
  80. def OAI.DimensionTen.Mod41.pow8_20 line 353
  81. def OAI.DimensionTen.Mod41.pow8_20_q line 355
  82. def OAI.DimensionTen.Mod41.pow8_20_mul_t line 357
  83. theorem OAI.DimensionTen.Mod41.pow8_20_mul_integer line 359
  84. theorem OAI.DimensionTen.Mod41.pow8_20_mul line 365
  85. theorem OAI.DimensionTen.Mod41.pow8_20_root line 371
  86. theorem OAI.DimensionTen.Mod41.pow8_20_pow line 376
  87. def OAI.DimensionTen.Mod41.pow8_40 line 384
  88. def OAI.DimensionTen.Mod41.pow8_40_q line 386
  89. def OAI.DimensionTen.Mod41.pow8_40_mul_t line 388
  90. theorem OAI.DimensionTen.Mod41.pow8_40_mul_integer line 390
  91. theorem OAI.DimensionTen.Mod41.pow8_40_mul line 396
  92. theorem OAI.DimensionTen.Mod41.pow8_40_root line 402
  93. theorem OAI.DimensionTen.Mod41.pow8_40_pow line 407
  94. def OAI.DimensionTen.Mod41.pow8_41 line 415
  95. def OAI.DimensionTen.Mod41.pow8_41_q line 417
  96. def OAI.DimensionTen.Mod41.pow8_41_mul_t line 419
  97. theorem OAI.DimensionTen.Mod41.pow8_41_mul_integer line 421
  98. theorem OAI.DimensionTen.Mod41.pow8_41_mul line 427
  99. theorem OAI.DimensionTen.Mod41.pow8_41_root line 433
  100. theorem OAI.DimensionTen.Mod41.pow8_41_pow line 438
  101. abbrev OAI.DimensionTen.Mod41.u8 line 444
  102. theorem OAI.DimensionTen.Mod41.iterate8 line 446