OAI/Analysis/Quantum/PPTSquare/Mod139Powers04.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P139.h741141964427589859983224276 line 12
  2. lemma OAI.ModularPencil.P139.h1482283928855179719966448551 line 16
  3. lemma OAI.ModularPencil.P139.h2964567857710359439932897101 line 20
  4. lemma OAI.ModularPencil.P139.h5929135715420718879865794202 line 24
  5. lemma OAI.ModularPencil.P139.h11858271430841437759731588404 line 28
  6. lemma OAI.ModularPencil.P139.h23716542861682875519463176808 line 32
  7. lemma OAI.ModularPencil.P139.h2964567857710359439932897102 line 36
  8. lemma OAI.ModularPencil.P139.h5929135715420718879865794203 line 40
  9. lemma OAI.ModularPencil.P139.h11858271430841437759731588405 line 44
  10. lemma OAI.ModularPencil.P139.h23716542861682875519463176809 line 48
  11. lemma OAI.ModularPencil.P139.h47433085723365751038926353617 line 52
  12. lemma OAI.ModularPencil.P139.h47433085723365751038926353618 line 56
  13. lemma OAI.ModularPencil.P139.h94866171446731502077852707235 line 60
  14. lemma OAI.ModularPencil.P139.h94866171446731502077852707236 line 64
  15. lemma OAI.ModularPencil.P139.h189732342893463004155705414471 line 68
  16. lemma OAI.ModularPencil.P139.h379464685786926008311410828942 line 72
  17. lemma OAI.ModularPencil.P139.h189732342893463004155705414472 line 76
  18. lemma OAI.ModularPencil.P139.h379464685786926008311410828943 line 80
  19. lemma OAI.ModularPencil.P139.h758929371573852016622821657885 line 84
  20. lemma OAI.ModularPencil.P139.h1517858743147704033245643315770 line 88
  21. lemma OAI.ModularPencil.P139.h758929371573852016622821657886 line 92
  22. lemma OAI.ModularPencil.P139.h1517858743147704033245643315771 line 96
  23. lemma OAI.ModularPencil.P139.h3035717486295408066491286631541 line 100
  24. lemma OAI.ModularPencil.P139.h3035717486295408066491286631542 line 104
  25. lemma OAI.ModularPencil.P139.h6071434972590816132982573263083 line 108
  26. lemma OAI.ModularPencil.P139.h12142869945181632265965146526166 line 112
  27. lemma OAI.ModularPencil.P139.h24285739890363264531930293052332 line 116
  28. lemma OAI.ModularPencil.P139.h6071434972590816132982573263084 line 120
  29. lemma OAI.ModularPencil.P139.h12142869945181632265965146526167 line 124
  30. lemma OAI.ModularPencil.P139.h24285739890363264531930293052333 line 128
  31. lemma OAI.ModularPencil.P139.h48571479780726529063860586104665 line 132
  32. lemma OAI.ModularPencil.P139.h48571479780726529063860586104666 line 136
  33. lemma OAI.ModularPencil.P139.h97142959561453058127721172209331 line 140
  34. lemma OAI.ModularPencil.P139.h97142959561453058127721172209332 line 144
  35. lemma OAI.ModularPencil.P139.h194285919122906116255442344418663 line 148
  36. lemma OAI.ModularPencil.P139.h388571838245812232510884688837326 line 152
  37. lemma OAI.ModularPencil.P139.h194285919122906116255442344418664 line 156
  38. lemma OAI.ModularPencil.P139.h388571838245812232510884688837327 line 160
  39. lemma OAI.ModularPencil.P139.h777143676491624465021769377674653 line 164
  40. lemma OAI.ModularPencil.P139.h777143676491624465021769377674654 line 168
  41. lemma OAI.ModularPencil.P139.h1554287352983248930043538755349307 line 172
  42. lemma OAI.ModularPencil.P139.h3108574705966497860087077510698614 line 176
  43. lemma OAI.ModularPencil.P139.h1554287352983248930043538755349308 line 180
  44. lemma OAI.ModularPencil.P139.h3108574705966497860087077510698615 line 184
  45. lemma OAI.ModularPencil.P139.h6217149411932995720174155021397229 line 188
  46. lemma OAI.ModularPencil.P139.h12434298823865991440348310042794458 line 192
  47. lemma OAI.ModularPencil.P139.h24868597647731982880696620085588916 line 196
  48. lemma OAI.ModularPencil.P139.h49737195295463965761393240171177832 line 200
  49. lemma OAI.ModularPencil.P139.h99474390590927931522786480342355664 line 204
  50. lemma OAI.ModularPencil.P139.h198948781181855863045572960684711328 line 208
  51. lemma OAI.ModularPencil.P139.h6217149411932995720174155021397230 line 212
  52. lemma OAI.ModularPencil.P139.h12434298823865991440348310042794459 line 216
  53. lemma OAI.ModularPencil.P139.h24868597647731982880696620085588917 line 220
  54. lemma OAI.ModularPencil.P139.h49737195295463965761393240171177833 line 224
  55. lemma OAI.ModularPencil.P139.h99474390590927931522786480342355665 line 228
  56. lemma OAI.ModularPencil.P139.h198948781181855863045572960684711329 line 232
  57. lemma OAI.ModularPencil.P139.h397897562363711726091145921369422657 line 236
  58. lemma OAI.ModularPencil.P139.h397897562363711726091145921369422658 line 240
  59. lemma OAI.ModularPencil.P139.h795795124727423452182291842738845315 line 244
  60. lemma OAI.ModularPencil.P139.h795795124727423452182291842738845316 line 248
  61. lemma OAI.ModularPencil.P139.h1591590249454846904364583685477690631 line 252
  62. lemma OAI.ModularPencil.P139.h1591590249454846904364583685477690632 line 256
  63. lemma OAI.ModularPencil.P139.h3183180498909693808729167370955381263 line 260
  64. lemma OAI.ModularPencil.P139.h3183180498909693808729167370955381264 line 264