OAI/Analysis/Quantum/PPTSquare/Mod41Powers06.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P41.h343642774498788699155864422 line 12
  2. lemma OAI.ModularPencil.P41.h687285548997577398311728843 line 16
  3. lemma OAI.ModularPencil.P41.h687285548997577398311728844 line 20
  4. lemma OAI.ModularPencil.P41.h1374571097995154796623457687 line 24
  5. lemma OAI.ModularPencil.P41.h1374571097995154796623457688 line 28
  6. lemma OAI.ModularPencil.P41.h2749142195990309593246915375 line 32
  7. lemma OAI.ModularPencil.P41.h2749142195990309593246915376 line 36
  8. lemma OAI.ModularPencil.P41.h5498284391980619186493830751 line 40
  9. lemma OAI.ModularPencil.P41.h10996568783961238372987661502 line 44
  10. lemma OAI.ModularPencil.P41.h5498284391980619186493830752 line 48
  11. lemma OAI.ModularPencil.P41.h10996568783961238372987661503 line 52
  12. lemma OAI.ModularPencil.P41.h21993137567922476745975323005 line 56
  13. lemma OAI.ModularPencil.P41.h21993137567922476745975323006 line 60
  14. lemma OAI.ModularPencil.P41.h43986275135844953491950646011 line 64
  15. lemma OAI.ModularPencil.P41.h43986275135844953491950646012 line 68
  16. lemma OAI.ModularPencil.P41.h87972550271689906983901292023 line 72
  17. lemma OAI.ModularPencil.P41.h87972550271689906983901292024 line 76
  18. lemma OAI.ModularPencil.P41.h175945100543379813967802584047 line 80
  19. lemma OAI.ModularPencil.P41.h175945100543379813967802584048 line 84
  20. lemma OAI.ModularPencil.P41.h351890201086759627935605168095 line 88
  21. lemma OAI.ModularPencil.P41.h703780402173519255871210336190 line 92
  22. lemma OAI.ModularPencil.P41.h351890201086759627935605168096 line 96
  23. lemma OAI.ModularPencil.P41.h703780402173519255871210336191 line 100
  24. lemma OAI.ModularPencil.P41.h1407560804347038511742420672381 line 104
  25. lemma OAI.ModularPencil.P41.h2815121608694077023484841344762 line 108
  26. lemma OAI.ModularPencil.P41.h1407560804347038511742420672382 line 112
  27. lemma OAI.ModularPencil.P41.h2815121608694077023484841344763 line 116
  28. lemma OAI.ModularPencil.P41.h5630243217388154046969682689525 line 120
  29. lemma OAI.ModularPencil.P41.h11260486434776308093939365379050 line 124
  30. lemma OAI.ModularPencil.P41.h22520972869552616187878730758100 line 128
  31. lemma OAI.ModularPencil.P41.h45041945739105232375757461516200 line 132
  32. lemma OAI.ModularPencil.P41.h90083891478210464751514923032400 line 136
  33. lemma OAI.ModularPencil.P41.h5630243217388154046969682689526 line 140
  34. lemma OAI.ModularPencil.P41.h11260486434776308093939365379051 line 144
  35. lemma OAI.ModularPencil.P41.h22520972869552616187878730758101 line 148
  36. lemma OAI.ModularPencil.P41.h45041945739105232375757461516201 line 152
  37. lemma OAI.ModularPencil.P41.h90083891478210464751514923032401 line 156
  38. lemma OAI.ModularPencil.P41.h180167782956420929503029846064801 line 160
  39. lemma OAI.ModularPencil.P41.gcd_degree20 line 164
  40. lemma OAI.ModularPencil.P41.derivative_f line 180
  41. lemma OAI.ModularPencil.P41.separable line 188