OAI/NumberTheory/Ostmann/Characters/TupleCRTFourier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact cofactor arguments for the Fourier transform of a prime tuple

  1. def OAI.Ostmann.tupleCofactor line 12
  2. theorem OAI.Ostmann.tupleCofactor_mul line 15
  3. theorem OAI.Ostmann.tupleCofactor_coprime line 19
  4. theorem OAI.Ostmann.stdAddChar_factor line 25
  5. theorem OAI.Ostmann.tuple_stdAddChar line 38
  6. def OAI.Ostmann.tupleCRTFunction line 77
  7. theorem OAI.Ostmann.tupleCRTFunction_intCast line 82
  8. theorem OAI.Ostmann.tupleCRTFunction_fourier line 88