OAI/NumberTheory/ZetaFive/Arithmetic/LargePrimeTable.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zeta5.Workers.W20.nm line 11
  2. def OAI.Zeta5.Workers.W20.nd line 13
  3. def OAI.Zeta5.Workers.W20.ns line 15
  4. def OAI.Zeta5.Workers.W20.ha line 17
  5. def OAI.Zeta5.Workers.W20.hs line 19
  6. def OAI.Zeta5.Workers.W20.ib line 21
  7. def OAI.Zeta5.Workers.W20.nbad line 23
  8. def OAI.Zeta5.Workers.W20.j0 line 25
  9. def OAI.Zeta5.Workers.W20.fInf line 27
  10. def OAI.Zeta5.Workers.W20.gInf line 29
  11. def OAI.Zeta5.Workers.W20.largePrimeLimit line 31
  12. theorem OAI.Zeta5.Workers.W20.piece_01 line 35
  13. theorem OAI.Zeta5.Workers.W20.piece_02 line 66
  14. theorem OAI.Zeta5.Workers.W20.piece_03 line 97
  15. theorem OAI.Zeta5.Workers.W20.piece_04 line 127
  16. theorem OAI.Zeta5.Workers.W20.piece_05 line 157
  17. theorem OAI.Zeta5.Workers.W20.piece_06 line 186
  18. theorem OAI.Zeta5.Workers.W20.piece_07 line 215
  19. theorem OAI.Zeta5.Workers.W20.piece_08 line 243