OAI/NumberTheory/Ostmann/Construction/PrimeTupleTranslation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Constructing the common translation for an actual tuple of primes

  1. def OAI.Ostmann.primeTupleSet line 15
  2. theorem OAI.Ostmann.primeTupleSet_subset line 18
  3. theorem OAI.Ostmann.primeTupleProduct_eq_set line 24
  4. theorem OAI.Ostmann.primeTupleProduct_squarefree line 31
  5. theorem OAI.Ostmann.primeTupleProduct_odd line 36
  6. theorem OAI.Ostmann.primeTupleProduct_one_lt line 42
  7. theorem OAI.Ostmann.exists_primeTuple_translation line 47
  8. theorem OAI.Ostmann.jacobi_primeTuple_translation line 87