OAI/NumberTheory/Ostmann/Arithmetic/HistoryCRTIntegrationModuli.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryCRTIntegration.rootModulus line 14
  2. def OAI.Ostmann.Arithmetic.HistoryCRTIntegration.outsideModulus line 15
  3. def OAI.Ostmann.Arithmetic.HistoryCRTIntegration.frequencyModulus line 16
  4. def OAI.Ostmann.Arithmetic.HistoryCRTIntegration.representativeModulus line 18
  5. def OAI.Ostmann.Arithmetic.HistoryCRTIntegration.historyModuli line 21
  6. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.historyModuli_prod line 25
  7. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.historyModuli_pairwise line 30
  8. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.rootModulus_pos line 35
  9. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.outsideModulus_pos line 41
  10. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.frequencyModulus_pos line 44
  11. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.representativeModulus_pos line 56
  12. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.historyModuli_pos line 61
  13. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.historyModuliNeZero line 71
  14. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.representativeSquaresNeZero line 76