OAI/Analysis/Quantum/PPTSquare/Mod131Powers04.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P131.h58734345041784888997510177654 line 12
  2. lemma OAI.ModularPencil.P131.h117468690083569777995020355308 line 16
  3. lemma OAI.ModularPencil.P131.h234937380167139555990040710616 line 20
  4. lemma OAI.ModularPencil.P131.h469874760334279111980081421232 line 24
  5. lemma OAI.ModularPencil.P131.h939749520668558223960162842464 line 28
  6. lemma OAI.ModularPencil.P131.h29367172520892444498755088828 line 32
  7. lemma OAI.ModularPencil.P131.h58734345041784888997510177655 line 36
  8. lemma OAI.ModularPencil.P131.h117468690083569777995020355309 line 40
  9. lemma OAI.ModularPencil.P131.h234937380167139555990040710617 line 44
  10. lemma OAI.ModularPencil.P131.h469874760334279111980081421233 line 48
  11. lemma OAI.ModularPencil.P131.h939749520668558223960162842465 line 52
  12. lemma OAI.ModularPencil.P131.h1879499041337116447920325684929 line 56
  13. lemma OAI.ModularPencil.P131.h1879499041337116447920325684930 line 60
  14. lemma OAI.ModularPencil.P131.h3758998082674232895840651369859 line 64
  15. lemma OAI.ModularPencil.P131.h3758998082674232895840651369860 line 68
  16. lemma OAI.ModularPencil.P131.h7517996165348465791681302739719 line 72
  17. lemma OAI.ModularPencil.P131.h15035992330696931583362605479438 line 76
  18. lemma OAI.ModularPencil.P131.h30071984661393863166725210958876 line 80
  19. lemma OAI.ModularPencil.P131.h60143969322787726333450421917752 line 84
  20. lemma OAI.ModularPencil.P131.h7517996165348465791681302739720 line 88
  21. lemma OAI.ModularPencil.P131.h15035992330696931583362605479439 line 92
  22. lemma OAI.ModularPencil.P131.h30071984661393863166725210958877 line 96
  23. lemma OAI.ModularPencil.P131.h60143969322787726333450421917753 line 100
  24. lemma OAI.ModularPencil.P131.h120287938645575452666900843835505 line 104
  25. lemma OAI.ModularPencil.P131.h240575877291150905333801687671010 line 108
  26. lemma OAI.ModularPencil.P131.h120287938645575452666900843835506 line 112
  27. lemma OAI.ModularPencil.P131.h240575877291150905333801687671011 line 116
  28. lemma OAI.ModularPencil.P131.h481151754582301810667603375342021 line 120
  29. lemma OAI.ModularPencil.P131.h481151754582301810667603375342022 line 124
  30. lemma OAI.ModularPencil.P131.h962303509164603621335206750684043 line 128
  31. lemma OAI.ModularPencil.P131.h962303509164603621335206750684044 line 132
  32. lemma OAI.ModularPencil.P131.h1924607018329207242670413501368087 line 136
  33. lemma OAI.ModularPencil.P131.h3849214036658414485340827002736174 line 140
  34. lemma OAI.ModularPencil.P131.h7698428073316828970681654005472348 line 144
  35. lemma OAI.ModularPencil.P131.h1924607018329207242670413501368088 line 148
  36. lemma OAI.ModularPencil.P131.h3849214036658414485340827002736175 line 152
  37. lemma OAI.ModularPencil.P131.h7698428073316828970681654005472349 line 156
  38. lemma OAI.ModularPencil.P131.h15396856146633657941363308010944697 line 160
  39. lemma OAI.ModularPencil.P131.h30793712293267315882726616021889394 line 164
  40. lemma OAI.ModularPencil.P131.h61587424586534631765453232043778788 line 168
  41. lemma OAI.ModularPencil.P131.h123174849173069263530906464087557576 line 172
  42. lemma OAI.ModularPencil.P131.h246349698346138527061812928175115152 line 176
  43. lemma OAI.ModularPencil.P131.h15396856146633657941363308010944698 line 180
  44. lemma OAI.ModularPencil.P131.h30793712293267315882726616021889395 line 184
  45. lemma OAI.ModularPencil.P131.h61587424586534631765453232043778789 line 188
  46. lemma OAI.ModularPencil.P131.h123174849173069263530906464087557577 line 192
  47. lemma OAI.ModularPencil.P131.h246349698346138527061812928175115153 line 196
  48. lemma OAI.ModularPencil.P131.h492699396692277054123625856350230305 line 200
  49. lemma OAI.ModularPencil.P131.h492699396692277054123625856350230306 line 204
  50. lemma OAI.ModularPencil.P131.h985398793384554108247251712700460611 line 208
  51. lemma OAI.ModularPencil.P131.gcd_degree17 line 212
  52. lemma OAI.ModularPencil.P131.derivative_f line 228
  53. lemma OAI.ModularPencil.P131.separable line 236