OAI/NumberTheory/Ostmann/Arithmetic/HistoryGiantOriginalMeanFactorizationDefs.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.Seed line 20
  2. abbrev OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.Current line 21
  3. abbrev OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.Choices line 22
  4. def OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.counterpart line 25
  5. def OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.originalPrimeMean line 33
  6. def OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.originalMixedMean line 41
  7. def OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.history line 50
  8. def OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.compensationFactor line 55
  9. theorem OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.compensationFactor_eq line 63
  10. theorem OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.history_small_split line 81
  11. theorem OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.prime_reference_factor line 88
  12. theorem OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.mixed_reference_factor line 107