OAI/Analysis/Quantum/PPTSquare/Mod41Powers02.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P41.h6103 line 12
  2. lemma OAI.ModularPencil.P41.h6104 line 16
  3. lemma OAI.ModularPencil.P41.h12207 line 20
  4. lemma OAI.ModularPencil.P41.h12208 line 24
  5. lemma OAI.ModularPencil.P41.h24415 line 28
  6. lemma OAI.ModularPencil.P41.h24416 line 32
  7. lemma OAI.ModularPencil.P41.h48831 line 36
  8. lemma OAI.ModularPencil.P41.h97662 line 40
  9. lemma OAI.ModularPencil.P41.h48832 line 44
  10. lemma OAI.ModularPencil.P41.h97663 line 48
  11. lemma OAI.ModularPencil.P41.h195325 line 52
  12. lemma OAI.ModularPencil.P41.h390650 line 56
  13. lemma OAI.ModularPencil.P41.h195326 line 60
  14. lemma OAI.ModularPencil.P41.h390651 line 64
  15. lemma OAI.ModularPencil.P41.h781301 line 68
  16. lemma OAI.ModularPencil.P41.h781302 line 72
  17. lemma OAI.ModularPencil.P41.h1562603 line 76
  18. lemma OAI.ModularPencil.P41.h3125206 line 80
  19. lemma OAI.ModularPencil.P41.h6250412 line 84
  20. lemma OAI.ModularPencil.P41.h1562604 line 88
  21. lemma OAI.ModularPencil.P41.h3125207 line 92
  22. lemma OAI.ModularPencil.P41.h6250413 line 96
  23. lemma OAI.ModularPencil.P41.h12500825 line 100
  24. lemma OAI.ModularPencil.P41.h12500826 line 104
  25. lemma OAI.ModularPencil.P41.h25001651 line 108
  26. lemma OAI.ModularPencil.P41.h50003302 line 112
  27. lemma OAI.ModularPencil.P41.h25001652 line 116
  28. lemma OAI.ModularPencil.P41.h50003303 line 120
  29. lemma OAI.ModularPencil.P41.h100006605 line 124
  30. lemma OAI.ModularPencil.P41.h200013210 line 128
  31. lemma OAI.ModularPencil.P41.h400026420 line 132
  32. lemma OAI.ModularPencil.P41.h800052840 line 136
  33. lemma OAI.ModularPencil.P41.h1600105680 line 140
  34. lemma OAI.ModularPencil.P41.h3200211360 line 144
  35. lemma OAI.ModularPencil.P41.h6400422720 line 148
  36. lemma OAI.ModularPencil.P41.h100006606 line 152
  37. lemma OAI.ModularPencil.P41.h200013211 line 156
  38. lemma OAI.ModularPencil.P41.h400026421 line 160
  39. lemma OAI.ModularPencil.P41.h800052841 line 164
  40. lemma OAI.ModularPencil.P41.h1600105681 line 168
  41. lemma OAI.ModularPencil.P41.h3200211361 line 172
  42. lemma OAI.ModularPencil.P41.h6400422721 line 176
  43. lemma OAI.ModularPencil.P41.h12800845441 line 180
  44. lemma OAI.ModularPencil.P41.h12800845442 line 184
  45. lemma OAI.ModularPencil.P41.h25601690883 line 188
  46. lemma OAI.ModularPencil.P41.h25601690884 line 192
  47. lemma OAI.ModularPencil.P41.h51203381767 line 196
  48. lemma OAI.ModularPencil.P41.h51203381768 line 200
  49. lemma OAI.ModularPencil.P41.h102406763535 line 204
  50. lemma OAI.ModularPencil.P41.h102406763536 line 208
  51. lemma OAI.ModularPencil.P41.h204813527071 line 212
  52. lemma OAI.ModularPencil.P41.h409627054142 line 216
  53. lemma OAI.ModularPencil.P41.h204813527072 line 220
  54. lemma OAI.ModularPencil.P41.h409627054143 line 224
  55. lemma OAI.ModularPencil.P41.h819254108285 line 228
  56. lemma OAI.ModularPencil.P41.h819254108286 line 232
  57. lemma OAI.ModularPencil.P41.h1638508216571 line 236
  58. lemma OAI.ModularPencil.P41.h3277016433142 line 240
  59. lemma OAI.ModularPencil.P41.h1638508216572 line 244
  60. lemma OAI.ModularPencil.P41.h3277016433143 line 248
  61. lemma OAI.ModularPencil.P41.h6554032866285 line 252
  62. lemma OAI.ModularPencil.P41.h13108065732570 line 256
  63. lemma OAI.ModularPencil.P41.h6554032866286 line 260
  64. lemma OAI.ModularPencil.P41.h13108065732571 line 264