OAI/Analysis/Quantum/PPTSquare/Mod131Powers02.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P131.h795998807 line 12
  2. lemma OAI.ModularPencil.P131.h1591997613 line 16
  3. lemma OAI.ModularPencil.P131.h3183995225 line 20
  4. lemma OAI.ModularPencil.P131.h6367990449 line 24
  5. lemma OAI.ModularPencil.P131.h12735980898 line 28
  6. lemma OAI.ModularPencil.P131.h6367990450 line 32
  7. lemma OAI.ModularPencil.P131.h12735980899 line 36
  8. lemma OAI.ModularPencil.P131.h25471961797 line 40
  9. lemma OAI.ModularPencil.P131.h25471961798 line 44
  10. lemma OAI.ModularPencil.P131.h50943923595 line 48
  11. lemma OAI.ModularPencil.P131.h101887847190 line 52
  12. lemma OAI.ModularPencil.P131.h203775694380 line 56
  13. lemma OAI.ModularPencil.P131.h407551388760 line 60
  14. lemma OAI.ModularPencil.P131.h815102777520 line 64
  15. lemma OAI.ModularPencil.P131.h50943923596 line 68
  16. lemma OAI.ModularPencil.P131.h101887847191 line 72
  17. lemma OAI.ModularPencil.P131.h203775694381 line 76
  18. lemma OAI.ModularPencil.P131.h407551388761 line 80
  19. lemma OAI.ModularPencil.P131.h815102777521 line 84
  20. lemma OAI.ModularPencil.P131.h1630205555041 line 88
  21. lemma OAI.ModularPencil.P131.h1630205555042 line 92
  22. lemma OAI.ModularPencil.P131.h3260411110083 line 96
  23. lemma OAI.ModularPencil.P131.h6520822220166 line 100
  24. lemma OAI.ModularPencil.P131.h3260411110084 line 104
  25. lemma OAI.ModularPencil.P131.h6520822220167 line 108
  26. lemma OAI.ModularPencil.P131.h13041644440333 line 112
  27. lemma OAI.ModularPencil.P131.h13041644440334 line 116
  28. lemma OAI.ModularPencil.P131.h26083288880667 line 120
  29. lemma OAI.ModularPencil.P131.h52166577761334 line 124
  30. lemma OAI.ModularPencil.P131.h104333155522668 line 128
  31. lemma OAI.ModularPencil.P131.h26083288880668 line 132
  32. lemma OAI.ModularPencil.P131.h52166577761335 line 136
  33. lemma OAI.ModularPencil.P131.h104333155522669 line 140
  34. lemma OAI.ModularPencil.P131.h208666311045337 line 144
  35. lemma OAI.ModularPencil.P131.h208666311045338 line 148
  36. lemma OAI.ModularPencil.P131.h417332622090675 line 152
  37. lemma OAI.ModularPencil.P131.h834665244181350 line 156
  38. lemma OAI.ModularPencil.P131.h1669330488362700 line 160
  39. lemma OAI.ModularPencil.P131.h3338660976725400 line 164
  40. lemma OAI.ModularPencil.P131.h417332622090676 line 168
  41. lemma OAI.ModularPencil.P131.h834665244181351 line 172
  42. lemma OAI.ModularPencil.P131.h1669330488362701 line 176
  43. lemma OAI.ModularPencil.P131.h3338660976725401 line 180
  44. lemma OAI.ModularPencil.P131.h6677321953450801 line 184
  45. lemma OAI.ModularPencil.P131.h6677321953450802 line 188
  46. lemma OAI.ModularPencil.P131.h13354643906901603 line 192
  47. lemma OAI.ModularPencil.P131.h26709287813803206 line 196
  48. lemma OAI.ModularPencil.P131.h13354643906901604 line 200
  49. lemma OAI.ModularPencil.P131.h26709287813803207 line 204
  50. lemma OAI.ModularPencil.P131.h53418575627606413 line 208
  51. lemma OAI.ModularPencil.P131.h53418575627606414 line 212
  52. lemma OAI.ModularPencil.P131.h106837151255212827 line 216
  53. lemma OAI.ModularPencil.P131.h106837151255212828 line 220
  54. lemma OAI.ModularPencil.P131.h213674302510425655 line 224
  55. lemma OAI.ModularPencil.P131.h213674302510425656 line 228
  56. lemma OAI.ModularPencil.P131.h427348605020851311 line 232
  57. lemma OAI.ModularPencil.P131.h427348605020851312 line 236
  58. lemma OAI.ModularPencil.P131.h854697210041702623 line 240
  59. lemma OAI.ModularPencil.P131.h1709394420083405246 line 244
  60. lemma OAI.ModularPencil.P131.h3418788840166810492 line 248
  61. lemma OAI.ModularPencil.P131.h6837577680333620984 line 252
  62. lemma OAI.ModularPencil.P131.h854697210041702624 line 256
  63. lemma OAI.ModularPencil.P131.h1709394420083405247 line 260
  64. lemma OAI.ModularPencil.P131.h3418788840166810493 line 264