OAI/NumberTheory/Ostmann/Quadratic/QuadraticSmallKernels.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact finite reindexing of the small-squarefree-kernel contribution

  1. theorem OAI.Ostmann.quadraticSquarePart_le line 12
  2. theorem OAI.Ostmann.quadraticSquarefreePart_dvd line 18
  3. theorem OAI.Ostmann.quadraticSquarePart_dvd line 21
  4. def OAI.Ostmann.quadraticSmallKernelRange line 25
  5. def OAI.Ostmann.quadraticSmallKernelPairs line 28
  6. theorem OAI.Ostmann.sum_quadraticSmallKernelRange line 32