OAI/Analysis/Quantum/PPTSquare/Mod139Powers01.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ModularPencil.P139.powerCert line 12
  2. lemma OAI.ModularPencil.P139.powerStep line 13
  3. def OAI.ModularPencil.P139.degreeCert line 17
  4. lemma OAI.ModularPencil.P139.degreeStep line 20
  5. lemma OAI.ModularPencil.P139.h1 line 25
  6. lemma OAI.ModularPencil.P139.h2 line 26
  7. lemma OAI.ModularPencil.P139.h4 line 30
  8. lemma OAI.ModularPencil.P139.h8 line 34
  9. lemma OAI.ModularPencil.P139.h3 line 38
  10. lemma OAI.ModularPencil.P139.h5 line 42
  11. lemma OAI.ModularPencil.P139.h9 line 46
  12. lemma OAI.ModularPencil.P139.h17 line 50
  13. lemma OAI.ModularPencil.P139.h34 line 54
  14. lemma OAI.ModularPencil.P139.h18 line 58
  15. lemma OAI.ModularPencil.P139.h35 line 62
  16. lemma OAI.ModularPencil.P139.h69 line 66
  17. lemma OAI.ModularPencil.P139.h70 line 70
  18. lemma OAI.ModularPencil.P139.h139 line 74
  19. lemma OAI.ModularPencil.P139.gcd_degree1 line 78
  20. lemma OAI.ModularPencil.P139.h10 line 94
  21. lemma OAI.ModularPencil.P139.h19 line 98
  22. lemma OAI.ModularPencil.P139.h38 line 102
  23. lemma OAI.ModularPencil.P139.h76 line 106
  24. lemma OAI.ModularPencil.P139.h20 line 110
  25. lemma OAI.ModularPencil.P139.h39 line 114
  26. lemma OAI.ModularPencil.P139.h77 line 118
  27. lemma OAI.ModularPencil.P139.h153 line 122
  28. lemma OAI.ModularPencil.P139.h306 line 126
  29. lemma OAI.ModularPencil.P139.h154 line 130
  30. lemma OAI.ModularPencil.P139.h307 line 134
  31. lemma OAI.ModularPencil.P139.h613 line 138
  32. lemma OAI.ModularPencil.P139.h1226 line 142
  33. lemma OAI.ModularPencil.P139.h2452 line 146
  34. lemma OAI.ModularPencil.P139.h4904 line 150
  35. lemma OAI.ModularPencil.P139.h9808 line 154
  36. lemma OAI.ModularPencil.P139.h614 line 158
  37. lemma OAI.ModularPencil.P139.h1227 line 162
  38. lemma OAI.ModularPencil.P139.h2453 line 166
  39. lemma OAI.ModularPencil.P139.h4905 line 170
  40. lemma OAI.ModularPencil.P139.h9809 line 174
  41. lemma OAI.ModularPencil.P139.h19617 line 178
  42. lemma OAI.ModularPencil.P139.h19618 line 182
  43. lemma OAI.ModularPencil.P139.h39235 line 186
  44. lemma OAI.ModularPencil.P139.h39236 line 190
  45. lemma OAI.ModularPencil.P139.h78471 line 194
  46. lemma OAI.ModularPencil.P139.h156942 line 198
  47. lemma OAI.ModularPencil.P139.h78472 line 202
  48. lemma OAI.ModularPencil.P139.h156943 line 206
  49. lemma OAI.ModularPencil.P139.h313885 line 210
  50. lemma OAI.ModularPencil.P139.h313886 line 214
  51. lemma OAI.ModularPencil.P139.h627771 line 218
  52. lemma OAI.ModularPencil.P139.h627772 line 222
  53. lemma OAI.ModularPencil.P139.h1255543 line 226
  54. lemma OAI.ModularPencil.P139.h2511086 line 230
  55. lemma OAI.ModularPencil.P139.h1255544 line 234
  56. lemma OAI.ModularPencil.P139.h2511087 line 238
  57. lemma OAI.ModularPencil.P139.h5022173 line 242
  58. lemma OAI.ModularPencil.P139.h10044346 line 246
  59. lemma OAI.ModularPencil.P139.h5022174 line 250
  60. lemma OAI.ModularPencil.P139.h10044347 line 254
  61. lemma OAI.ModularPencil.P139.h20088693 line 258
  62. lemma OAI.ModularPencil.P139.h40177386 line 262
  63. lemma OAI.ModularPencil.P139.h80354772 line 266
  64. lemma OAI.ModularPencil.P139.h20088694 line 270