OAI/Analysis/Quantum/PPTSquare/Mod41Powers03.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P41.h26216131465141 line 12
  2. lemma OAI.ModularPencil.P41.h52432262930282 line 16
  3. lemma OAI.ModularPencil.P41.h26216131465142 line 20
  4. lemma OAI.ModularPencil.P41.h52432262930283 line 24
  5. lemma OAI.ModularPencil.P41.h104864525860565 line 28
  6. lemma OAI.ModularPencil.P41.h104864525860566 line 32
  7. lemma OAI.ModularPencil.P41.h209729051721131 line 36
  8. lemma OAI.ModularPencil.P41.h419458103442262 line 40
  9. lemma OAI.ModularPencil.P41.h209729051721132 line 44
  10. lemma OAI.ModularPencil.P41.h419458103442263 line 48
  11. lemma OAI.ModularPencil.P41.h838916206884525 line 52
  12. lemma OAI.ModularPencil.P41.h1677832413769050 line 56
  13. lemma OAI.ModularPencil.P41.h3355664827538100 line 60
  14. lemma OAI.ModularPencil.P41.h6711329655076200 line 64
  15. lemma OAI.ModularPencil.P41.h838916206884526 line 68
  16. lemma OAI.ModularPencil.P41.h1677832413769051 line 72
  17. lemma OAI.ModularPencil.P41.h3355664827538101 line 76
  18. lemma OAI.ModularPencil.P41.h6711329655076201 line 80
  19. lemma OAI.ModularPencil.P41.h13422659310152401 line 84
  20. lemma OAI.ModularPencil.P41.gcd_degree10 line 88
  21. lemma OAI.ModularPencil.P41.h4 line 104
  22. lemma OAI.ModularPencil.P41.h8 line 108
  23. lemma OAI.ModularPencil.P41.h9 line 112
  24. lemma OAI.ModularPencil.P41.h17 line 116
  25. lemma OAI.ModularPencil.P41.h18 line 120
  26. lemma OAI.ModularPencil.P41.h35 line 124
  27. lemma OAI.ModularPencil.P41.h36 line 128
  28. lemma OAI.ModularPencil.P41.h71 line 132
  29. lemma OAI.ModularPencil.P41.h142 line 136
  30. lemma OAI.ModularPencil.P41.h284 line 140
  31. lemma OAI.ModularPencil.P41.h568 line 144
  32. lemma OAI.ModularPencil.P41.h72 line 148
  33. lemma OAI.ModularPencil.P41.h143 line 152
  34. lemma OAI.ModularPencil.P41.h285 line 156
  35. lemma OAI.ModularPencil.P41.h569 line 160
  36. lemma OAI.ModularPencil.P41.h1137 line 164
  37. lemma OAI.ModularPencil.P41.h2274 line 168
  38. lemma OAI.ModularPencil.P41.h4548 line 172
  39. lemma OAI.ModularPencil.P41.h9096 line 176
  40. lemma OAI.ModularPencil.P41.h18192 line 180
  41. lemma OAI.ModularPencil.P41.h36384 line 184
  42. lemma OAI.ModularPencil.P41.h1138 line 188
  43. lemma OAI.ModularPencil.P41.h2275 line 192
  44. lemma OAI.ModularPencil.P41.h4549 line 196
  45. lemma OAI.ModularPencil.P41.h9097 line 200
  46. lemma OAI.ModularPencil.P41.h18193 line 204
  47. lemma OAI.ModularPencil.P41.h36385 line 208
  48. lemma OAI.ModularPencil.P41.h72769 line 212
  49. lemma OAI.ModularPencil.P41.h145538 line 216
  50. lemma OAI.ModularPencil.P41.h291076 line 220
  51. lemma OAI.ModularPencil.P41.h72770 line 224
  52. lemma OAI.ModularPencil.P41.h145539 line 228
  53. lemma OAI.ModularPencil.P41.h291077 line 232
  54. lemma OAI.ModularPencil.P41.h582153 line 236
  55. lemma OAI.ModularPencil.P41.h582154 line 240
  56. lemma OAI.ModularPencil.P41.h1164307 line 244
  57. lemma OAI.ModularPencil.P41.h2328614 line 248
  58. lemma OAI.ModularPencil.P41.h4657228 line 252
  59. lemma OAI.ModularPencil.P41.h9314456 line 256
  60. lemma OAI.ModularPencil.P41.h18628912 line 260
  61. lemma OAI.ModularPencil.P41.h37257824 line 264
  62. lemma OAI.ModularPencil.P41.h74515648 line 268
  63. lemma OAI.ModularPencil.P41.h1164308 line 272
  64. lemma OAI.ModularPencil.P41.h2328615 line 276