OAI/NumberTheory/Ostmann/Construction/FixedPivotFormulas.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Removing the fixed pivot from the independent polynomial variables

  1. def OAI.Ostmann.HistoryFormula.fixNone line 11
  2. theorem OAI.Ostmann.HistoryFormula.fixNone_value line 14
  3. theorem OAI.Ostmann.HistoryFormula.fixNone_cost line 22
  4. theorem OAI.Ostmann.HistoryFormula.fixNone_frequencies line 32
  5. theorem OAI.Ostmann.HistoryFormula.fixNone_denominator line 40
  6. theorem OAI.Ostmann.HistoryFormula.fixNone_inputs line 44
  7. def OAI.Ostmann.HistoryFormula.fixedOriginalPrimes line 53
  8. theorem OAI.Ostmann.HistoryFormula.fixedOriginalPrimes_value line 57
  9. theorem OAI.Ostmann.HistoryFormula.fixedOriginalPrimes_cost line 70
  10. theorem OAI.Ostmann.HistoryFormula.fixedOriginalPrimes_denominator line 75
  11. theorem OAI.Ostmann.HistoryFormula.fixedOriginalPrimes_inputs line 80
  12. theorem OAI.Ostmann.HistoryFormula.fixedOriginalPrimes_integer_value line 86