OAI/Analysis/Quantum/PPTSquare/Mod131Powers01.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ModularPencil.P131.powerCert line 12
  2. lemma OAI.ModularPencil.P131.powerStep line 13
  3. def OAI.ModularPencil.P131.degreeCert line 17
  4. lemma OAI.ModularPencil.P131.degreeStep line 20
  5. lemma OAI.ModularPencil.P131.h1 line 25
  6. lemma OAI.ModularPencil.P131.h2 line 26
  7. lemma OAI.ModularPencil.P131.h3 line 30
  8. lemma OAI.ModularPencil.P131.h5 line 34
  9. lemma OAI.ModularPencil.P131.h6 line 38
  10. lemma OAI.ModularPencil.P131.h11 line 42
  11. lemma OAI.ModularPencil.P131.h12 line 46
  12. lemma OAI.ModularPencil.P131.h23 line 50
  13. lemma OAI.ModularPencil.P131.h24 line 54
  14. lemma OAI.ModularPencil.P131.h47 line 58
  15. lemma OAI.ModularPencil.P131.h94 line 62
  16. lemma OAI.ModularPencil.P131.h48 line 66
  17. lemma OAI.ModularPencil.P131.h95 line 70
  18. lemma OAI.ModularPencil.P131.h189 line 74
  19. lemma OAI.ModularPencil.P131.h190 line 78
  20. lemma OAI.ModularPencil.P131.h379 line 82
  21. lemma OAI.ModularPencil.P131.h380 line 86
  22. lemma OAI.ModularPencil.P131.h759 line 90
  23. lemma OAI.ModularPencil.P131.h1518 line 94
  24. lemma OAI.ModularPencil.P131.h3036 line 98
  25. lemma OAI.ModularPencil.P131.h6072 line 102
  26. lemma OAI.ModularPencil.P131.h760 line 106
  27. lemma OAI.ModularPencil.P131.h1519 line 110
  28. lemma OAI.ModularPencil.P131.h3037 line 114
  29. lemma OAI.ModularPencil.P131.h6073 line 118
  30. lemma OAI.ModularPencil.P131.h12145 line 122
  31. lemma OAI.ModularPencil.P131.h12146 line 126
  32. lemma OAI.ModularPencil.P131.h24291 line 130
  33. lemma OAI.ModularPencil.P131.h24292 line 134
  34. lemma OAI.ModularPencil.P131.h48583 line 138
  35. lemma OAI.ModularPencil.P131.h48584 line 142
  36. lemma OAI.ModularPencil.P131.h97167 line 146
  37. lemma OAI.ModularPencil.P131.h97168 line 150
  38. lemma OAI.ModularPencil.P131.h194335 line 154
  39. lemma OAI.ModularPencil.P131.h194336 line 158
  40. lemma OAI.ModularPencil.P131.h388671 line 162
  41. lemma OAI.ModularPencil.P131.h777342 line 166
  42. lemma OAI.ModularPencil.P131.h388672 line 170
  43. lemma OAI.ModularPencil.P131.h777343 line 174
  44. lemma OAI.ModularPencil.P131.h1554685 line 178
  45. lemma OAI.ModularPencil.P131.h3109370 line 182
  46. lemma OAI.ModularPencil.P131.h6218740 line 186
  47. lemma OAI.ModularPencil.P131.h1554686 line 190
  48. lemma OAI.ModularPencil.P131.h3109371 line 194
  49. lemma OAI.ModularPencil.P131.h6218741 line 198
  50. lemma OAI.ModularPencil.P131.h12437481 line 202
  51. lemma OAI.ModularPencil.P131.h24874962 line 206
  52. lemma OAI.ModularPencil.P131.h12437482 line 210
  53. lemma OAI.ModularPencil.P131.h24874963 line 214
  54. lemma OAI.ModularPencil.P131.h49749925 line 218
  55. lemma OAI.ModularPencil.P131.h99499850 line 222
  56. lemma OAI.ModularPencil.P131.h49749926 line 226
  57. lemma OAI.ModularPencil.P131.h99499851 line 230
  58. lemma OAI.ModularPencil.P131.h198999701 line 234
  59. lemma OAI.ModularPencil.P131.h198999702 line 238
  60. lemma OAI.ModularPencil.P131.h397999403 line 242
  61. lemma OAI.ModularPencil.P131.h795998806 line 246
  62. lemma OAI.ModularPencil.P131.h1591997612 line 250
  63. lemma OAI.ModularPencil.P131.h3183995224 line 254
  64. lemma OAI.ModularPencil.P131.h397999404 line 258