OAI/Analysis/Quantum/DimensionTen/Mod139Powers10.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Mod139.pow19_2 line 8
  2. def OAI.DimensionTen.Mod139.pow19_2_q line 10
  3. def OAI.DimensionTen.Mod139.pow19_2_mul_t line 12
  4. theorem OAI.DimensionTen.Mod139.pow19_2_mul_integer line 14
  5. theorem OAI.DimensionTen.Mod139.pow19_2_mul line 20
  6. theorem OAI.DimensionTen.Mod139.pow19_2_root line 26
  7. theorem OAI.DimensionTen.Mod139.pow19_2_pow line 31
  8. def OAI.DimensionTen.Mod139.pow19_4 line 39
  9. def OAI.DimensionTen.Mod139.pow19_4_q line 41
  10. def OAI.DimensionTen.Mod139.pow19_4_mul_t line 43
  11. theorem OAI.DimensionTen.Mod139.pow19_4_mul_integer line 45
  12. theorem OAI.DimensionTen.Mod139.pow19_4_mul line 51
  13. theorem OAI.DimensionTen.Mod139.pow19_4_root line 57
  14. theorem OAI.DimensionTen.Mod139.pow19_4_pow line 62
  15. def OAI.DimensionTen.Mod139.pow19_8 line 70
  16. def OAI.DimensionTen.Mod139.pow19_8_q line 72
  17. def OAI.DimensionTen.Mod139.pow19_8_mul_t line 74
  18. theorem OAI.DimensionTen.Mod139.pow19_8_mul_integer line 76
  19. theorem OAI.DimensionTen.Mod139.pow19_8_mul line 82
  20. theorem OAI.DimensionTen.Mod139.pow19_8_root line 88
  21. theorem OAI.DimensionTen.Mod139.pow19_8_pow line 93
  22. def OAI.DimensionTen.Mod139.pow19_16 line 101
  23. def OAI.DimensionTen.Mod139.pow19_16_q line 103
  24. def OAI.DimensionTen.Mod139.pow19_16_mul_t line 105
  25. theorem OAI.DimensionTen.Mod139.pow19_16_mul_integer line 107
  26. theorem OAI.DimensionTen.Mod139.pow19_16_mul line 113
  27. theorem OAI.DimensionTen.Mod139.pow19_16_root line 119
  28. theorem OAI.DimensionTen.Mod139.pow19_16_pow line 124
  29. def OAI.DimensionTen.Mod139.pow19_17 line 132
  30. def OAI.DimensionTen.Mod139.pow19_17_q line 134
  31. def OAI.DimensionTen.Mod139.pow19_17_mul_t line 136
  32. theorem OAI.DimensionTen.Mod139.pow19_17_mul_integer line 138
  33. theorem OAI.DimensionTen.Mod139.pow19_17_mul line 144
  34. theorem OAI.DimensionTen.Mod139.pow19_17_root line 150
  35. theorem OAI.DimensionTen.Mod139.pow19_17_pow line 155
  36. def OAI.DimensionTen.Mod139.pow19_34 line 161
  37. def OAI.DimensionTen.Mod139.pow19_34_q line 163
  38. def OAI.DimensionTen.Mod139.pow19_34_mul_t line 165
  39. theorem OAI.DimensionTen.Mod139.pow19_34_mul_integer line 167
  40. theorem OAI.DimensionTen.Mod139.pow19_34_mul line 173
  41. theorem OAI.DimensionTen.Mod139.pow19_34_root line 179
  42. theorem OAI.DimensionTen.Mod139.pow19_34_pow line 184
  43. def OAI.DimensionTen.Mod139.pow19_68 line 192
  44. def OAI.DimensionTen.Mod139.pow19_68_q line 194
  45. def OAI.DimensionTen.Mod139.pow19_68_mul_t line 196
  46. theorem OAI.DimensionTen.Mod139.pow19_68_mul_integer line 198
  47. theorem OAI.DimensionTen.Mod139.pow19_68_mul line 204
  48. theorem OAI.DimensionTen.Mod139.pow19_68_root line 210
  49. theorem OAI.DimensionTen.Mod139.pow19_68_pow line 215
  50. def OAI.DimensionTen.Mod139.pow19_69 line 223
  51. def OAI.DimensionTen.Mod139.pow19_69_q line 225
  52. def OAI.DimensionTen.Mod139.pow19_69_mul_t line 227
  53. theorem OAI.DimensionTen.Mod139.pow19_69_mul_integer line 229
  54. theorem OAI.DimensionTen.Mod139.pow19_69_mul line 235
  55. theorem OAI.DimensionTen.Mod139.pow19_69_root line 241
  56. theorem OAI.DimensionTen.Mod139.pow19_69_pow line 246
  57. def OAI.DimensionTen.Mod139.pow19_138 line 252
  58. def OAI.DimensionTen.Mod139.pow19_138_q line 254
  59. def OAI.DimensionTen.Mod139.pow19_138_mul_t line 256
  60. theorem OAI.DimensionTen.Mod139.pow19_138_mul_integer line 258
  61. theorem OAI.DimensionTen.Mod139.pow19_138_mul line 264
  62. theorem OAI.DimensionTen.Mod139.pow19_138_root line 270
  63. theorem OAI.DimensionTen.Mod139.pow19_138_pow line 275
  64. abbrev OAI.DimensionTen.Mod139.pow19_139 line 283
  65. def OAI.DimensionTen.Mod139.pow19_139_q line 285
  66. def OAI.DimensionTen.Mod139.pow19_139_mul_t line 287
  67. theorem OAI.DimensionTen.Mod139.pow19_139_mul_integer line 289
  68. theorem OAI.DimensionTen.Mod139.pow19_139_mul line 295
  69. theorem OAI.DimensionTen.Mod139.pow19_139_root line 301
  70. theorem OAI.DimensionTen.Mod139.pow19_139_pow line 306
  71. abbrev OAI.DimensionTen.Mod139.u19 line 312
  72. theorem OAI.DimensionTen.Mod139.iterate19 line 314