OAI/Analysis/Quantum/PPTSquare/Mod41Powers01.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ModularPencil.P41.powerCert line 12
  2. lemma OAI.ModularPencil.P41.powerStep line 13
  3. def OAI.ModularPencil.P41.degreeCert line 17
  4. lemma OAI.ModularPencil.P41.degreeStep line 20
  5. lemma OAI.ModularPencil.P41.h1 line 25
  6. lemma OAI.ModularPencil.P41.h2 line 26
  7. lemma OAI.ModularPencil.P41.h3 line 30
  8. lemma OAI.ModularPencil.P41.h5 line 34
  9. lemma OAI.ModularPencil.P41.h10 line 38
  10. lemma OAI.ModularPencil.P41.h6 line 42
  11. lemma OAI.ModularPencil.P41.h11 line 46
  12. lemma OAI.ModularPencil.P41.h21 line 50
  13. lemma OAI.ModularPencil.P41.h22 line 54
  14. lemma OAI.ModularPencil.P41.h43 line 58
  15. lemma OAI.ModularPencil.P41.h86 line 62
  16. lemma OAI.ModularPencil.P41.h172 line 66
  17. lemma OAI.ModularPencil.P41.h344 line 70
  18. lemma OAI.ModularPencil.P41.h44 line 74
  19. lemma OAI.ModularPencil.P41.h87 line 78
  20. lemma OAI.ModularPencil.P41.h173 line 82
  21. lemma OAI.ModularPencil.P41.h345 line 86
  22. lemma OAI.ModularPencil.P41.h689 line 90
  23. lemma OAI.ModularPencil.P41.h690 line 94
  24. lemma OAI.ModularPencil.P41.h1379 line 98
  25. lemma OAI.ModularPencil.P41.h1380 line 102
  26. lemma OAI.ModularPencil.P41.h2759 line 106
  27. lemma OAI.ModularPencil.P41.h2760 line 110
  28. lemma OAI.ModularPencil.P41.h5519 line 114
  29. lemma OAI.ModularPencil.P41.h11038 line 118
  30. lemma OAI.ModularPencil.P41.h22076 line 122
  31. lemma OAI.ModularPencil.P41.h44152 line 126
  32. lemma OAI.ModularPencil.P41.h5520 line 130
  33. lemma OAI.ModularPencil.P41.h11039 line 134
  34. lemma OAI.ModularPencil.P41.h22077 line 138
  35. lemma OAI.ModularPencil.P41.h44153 line 142
  36. lemma OAI.ModularPencil.P41.h88305 line 146
  37. lemma OAI.ModularPencil.P41.h176610 line 150
  38. lemma OAI.ModularPencil.P41.h353220 line 154
  39. lemma OAI.ModularPencil.P41.h706440 line 158
  40. lemma OAI.ModularPencil.P41.h1412880 line 162
  41. lemma OAI.ModularPencil.P41.h88306 line 166
  42. lemma OAI.ModularPencil.P41.h176611 line 170
  43. lemma OAI.ModularPencil.P41.h353221 line 174
  44. lemma OAI.ModularPencil.P41.h706441 line 178
  45. lemma OAI.ModularPencil.P41.h1412881 line 182
  46. lemma OAI.ModularPencil.P41.h2825761 line 186
  47. lemma OAI.ModularPencil.P41.gcd_degree4 line 190
  48. lemma OAI.ModularPencil.P41.h12 line 206
  49. lemma OAI.ModularPencil.P41.h23 line 210
  50. lemma OAI.ModularPencil.P41.h24 line 214
  51. lemma OAI.ModularPencil.P41.h47 line 218
  52. lemma OAI.ModularPencil.P41.h48 line 222
  53. lemma OAI.ModularPencil.P41.h95 line 226
  54. lemma OAI.ModularPencil.P41.h190 line 230
  55. lemma OAI.ModularPencil.P41.h96 line 234
  56. lemma OAI.ModularPencil.P41.h191 line 238
  57. lemma OAI.ModularPencil.P41.h381 line 242
  58. lemma OAI.ModularPencil.P41.h762 line 246
  59. lemma OAI.ModularPencil.P41.h382 line 250
  60. lemma OAI.ModularPencil.P41.h763 line 254
  61. lemma OAI.ModularPencil.P41.h1525 line 258
  62. lemma OAI.ModularPencil.P41.h1526 line 262
  63. lemma OAI.ModularPencil.P41.h3051 line 266
  64. lemma OAI.ModularPencil.P41.h3052 line 270