OAI/Analysis/Quantum/PPTSquare/Mod41Powers05.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P41.h80010568373554549 line 12
  2. lemma OAI.ModularPencil.P41.h160021136747109097 line 16
  3. lemma OAI.ModularPencil.P41.h160021136747109098 line 20
  4. lemma OAI.ModularPencil.P41.h320042273494218195 line 24
  5. lemma OAI.ModularPencil.P41.h320042273494218196 line 28
  6. lemma OAI.ModularPencil.P41.h640084546988436391 line 32
  7. lemma OAI.ModularPencil.P41.h640084546988436392 line 36
  8. lemma OAI.ModularPencil.P41.h1280169093976872783 line 40
  9. lemma OAI.ModularPencil.P41.h1280169093976872784 line 44
  10. lemma OAI.ModularPencil.P41.h2560338187953745567 line 48
  11. lemma OAI.ModularPencil.P41.h5120676375907491134 line 52
  12. lemma OAI.ModularPencil.P41.h2560338187953745568 line 56
  13. lemma OAI.ModularPencil.P41.h5120676375907491135 line 60
  14. lemma OAI.ModularPencil.P41.h10241352751814982269 line 64
  15. lemma OAI.ModularPencil.P41.h10241352751814982270 line 68
  16. lemma OAI.ModularPencil.P41.h20482705503629964539 line 72
  17. lemma OAI.ModularPencil.P41.h20482705503629964540 line 76
  18. lemma OAI.ModularPencil.P41.h40965411007259929079 line 80
  19. lemma OAI.ModularPencil.P41.h40965411007259929080 line 84
  20. lemma OAI.ModularPencil.P41.h81930822014519858159 line 88
  21. lemma OAI.ModularPencil.P41.h163861644029039716318 line 92
  22. lemma OAI.ModularPencil.P41.h327723288058079432636 line 96
  23. lemma OAI.ModularPencil.P41.h655446576116158865272 line 100
  24. lemma OAI.ModularPencil.P41.h1310893152232317730544 line 104
  25. lemma OAI.ModularPencil.P41.h81930822014519858160 line 108
  26. lemma OAI.ModularPencil.P41.h163861644029039716319 line 112
  27. lemma OAI.ModularPencil.P41.h327723288058079432637 line 116
  28. lemma OAI.ModularPencil.P41.h655446576116158865273 line 120
  29. lemma OAI.ModularPencil.P41.h1310893152232317730545 line 124
  30. lemma OAI.ModularPencil.P41.h2621786304464635461089 line 128
  31. lemma OAI.ModularPencil.P41.h5243572608929270922178 line 132
  32. lemma OAI.ModularPencil.P41.h10487145217858541844356 line 136
  33. lemma OAI.ModularPencil.P41.h20974290435717083688712 line 140
  34. lemma OAI.ModularPencil.P41.h41948580871434167377424 line 144
  35. lemma OAI.ModularPencil.P41.h2621786304464635461090 line 148
  36. lemma OAI.ModularPencil.P41.h5243572608929270922179 line 152
  37. lemma OAI.ModularPencil.P41.h10487145217858541844357 line 156
  38. lemma OAI.ModularPencil.P41.h20974290435717083688713 line 160
  39. lemma OAI.ModularPencil.P41.h41948580871434167377425 line 164
  40. lemma OAI.ModularPencil.P41.h83897161742868334754849 line 168
  41. lemma OAI.ModularPencil.P41.h83897161742868334754850 line 172
  42. lemma OAI.ModularPencil.P41.h167794323485736669509699 line 176
  43. lemma OAI.ModularPencil.P41.h335588646971473339019398 line 180
  44. lemma OAI.ModularPencil.P41.h167794323485736669509700 line 184
  45. lemma OAI.ModularPencil.P41.h335588646971473339019399 line 188
  46. lemma OAI.ModularPencil.P41.h671177293942946678038797 line 192
  47. lemma OAI.ModularPencil.P41.h671177293942946678038798 line 196
  48. lemma OAI.ModularPencil.P41.h1342354587885893356077595 line 200
  49. lemma OAI.ModularPencil.P41.h2684709175771786712155190 line 204
  50. lemma OAI.ModularPencil.P41.h1342354587885893356077596 line 208
  51. lemma OAI.ModularPencil.P41.h2684709175771786712155191 line 212
  52. lemma OAI.ModularPencil.P41.h5369418351543573424310381 line 216
  53. lemma OAI.ModularPencil.P41.h5369418351543573424310382 line 220
  54. lemma OAI.ModularPencil.P41.h10738836703087146848620763 line 224
  55. lemma OAI.ModularPencil.P41.h21477673406174293697241526 line 228
  56. lemma OAI.ModularPencil.P41.h42955346812348587394483052 line 232
  57. lemma OAI.ModularPencil.P41.h10738836703087146848620764 line 236
  58. lemma OAI.ModularPencil.P41.h21477673406174293697241527 line 240
  59. lemma OAI.ModularPencil.P41.h42955346812348587394483053 line 244
  60. lemma OAI.ModularPencil.P41.h85910693624697174788966105 line 248
  61. lemma OAI.ModularPencil.P41.h171821387249394349577932210 line 252
  62. lemma OAI.ModularPencil.P41.h85910693624697174788966106 line 256
  63. lemma OAI.ModularPencil.P41.h171821387249394349577932211 line 260
  64. lemma OAI.ModularPencil.P41.h343642774498788699155864421 line 264