OAI/Analysis/Quantum/PPTSquare/Mod41Powers04.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P41.h4657229 line 12
  2. lemma OAI.ModularPencil.P41.h9314457 line 16
  3. lemma OAI.ModularPencil.P41.h18628913 line 20
  4. lemma OAI.ModularPencil.P41.h37257825 line 24
  5. lemma OAI.ModularPencil.P41.h74515649 line 28
  6. lemma OAI.ModularPencil.P41.h149031297 line 32
  7. lemma OAI.ModularPencil.P41.h298062594 line 36
  8. lemma OAI.ModularPencil.P41.h596125188 line 40
  9. lemma OAI.ModularPencil.P41.h1192250376 line 44
  10. lemma OAI.ModularPencil.P41.h149031298 line 48
  11. lemma OAI.ModularPencil.P41.h298062595 line 52
  12. lemma OAI.ModularPencil.P41.h596125189 line 56
  13. lemma OAI.ModularPencil.P41.h1192250377 line 60
  14. lemma OAI.ModularPencil.P41.h2384500753 line 64
  15. lemma OAI.ModularPencil.P41.h4769001506 line 68
  16. lemma OAI.ModularPencil.P41.h9538003012 line 72
  17. lemma OAI.ModularPencil.P41.h19076006024 line 76
  18. lemma OAI.ModularPencil.P41.h2384500754 line 80
  19. lemma OAI.ModularPencil.P41.h4769001507 line 84
  20. lemma OAI.ModularPencil.P41.h9538003013 line 88
  21. lemma OAI.ModularPencil.P41.h19076006025 line 92
  22. lemma OAI.ModularPencil.P41.h38152012049 line 96
  23. lemma OAI.ModularPencil.P41.h76304024098 line 100
  24. lemma OAI.ModularPencil.P41.h38152012050 line 104
  25. lemma OAI.ModularPencil.P41.h76304024099 line 108
  26. lemma OAI.ModularPencil.P41.h152608048197 line 112
  27. lemma OAI.ModularPencil.P41.h152608048198 line 116
  28. lemma OAI.ModularPencil.P41.h305216096395 line 120
  29. lemma OAI.ModularPencil.P41.h305216096396 line 124
  30. lemma OAI.ModularPencil.P41.h610432192791 line 128
  31. lemma OAI.ModularPencil.P41.h1220864385582 line 132
  32. lemma OAI.ModularPencil.P41.h610432192792 line 136
  33. lemma OAI.ModularPencil.P41.h1220864385583 line 140
  34. lemma OAI.ModularPencil.P41.h2441728771165 line 144
  35. lemma OAI.ModularPencil.P41.h2441728771166 line 148
  36. lemma OAI.ModularPencil.P41.h4883457542331 line 152
  37. lemma OAI.ModularPencil.P41.h9766915084662 line 156
  38. lemma OAI.ModularPencil.P41.h19533830169324 line 160
  39. lemma OAI.ModularPencil.P41.h4883457542332 line 164
  40. lemma OAI.ModularPencil.P41.h9766915084663 line 168
  41. lemma OAI.ModularPencil.P41.h19533830169325 line 172
  42. lemma OAI.ModularPencil.P41.h39067660338649 line 176
  43. lemma OAI.ModularPencil.P41.h39067660338650 line 180
  44. lemma OAI.ModularPencil.P41.h78135320677299 line 184
  45. lemma OAI.ModularPencil.P41.h156270641354598 line 188
  46. lemma OAI.ModularPencil.P41.h78135320677300 line 192
  47. lemma OAI.ModularPencil.P41.h156270641354599 line 196
  48. lemma OAI.ModularPencil.P41.h312541282709197 line 200
  49. lemma OAI.ModularPencil.P41.h625082565418394 line 204
  50. lemma OAI.ModularPencil.P41.h312541282709198 line 208
  51. lemma OAI.ModularPencil.P41.h625082565418395 line 212
  52. lemma OAI.ModularPencil.P41.h1250165130836789 line 216
  53. lemma OAI.ModularPencil.P41.h1250165130836790 line 220
  54. lemma OAI.ModularPencil.P41.h2500330261673579 line 224
  55. lemma OAI.ModularPencil.P41.h2500330261673580 line 228
  56. lemma OAI.ModularPencil.P41.h5000660523347159 line 232
  57. lemma OAI.ModularPencil.P41.h10001321046694318 line 236
  58. lemma OAI.ModularPencil.P41.h5000660523347160 line 240
  59. lemma OAI.ModularPencil.P41.h10001321046694319 line 244
  60. lemma OAI.ModularPencil.P41.h20002642093388637 line 248
  61. lemma OAI.ModularPencil.P41.h40005284186777274 line 252
  62. lemma OAI.ModularPencil.P41.h80010568373554548 line 256
  63. lemma OAI.ModularPencil.P41.h20002642093388638 line 260
  64. lemma OAI.ModularPencil.P41.h40005284186777275 line 264