OAI/NumberTheory/Ostmann/Arithmetic/HistoryProductWindowsNominal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.pruned_append line 11
  2. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.remainder_sourceBlock line 17
  3. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.extracted_sourceBlock line 35
  4. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.pruned_sourceBlock_bulk line 53
  5. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.pruned_sourceBlock_top line 59
  6. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.pruned_sourceBlock_comp line 65
  7. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.sourceSum_fixedCenter_bulk line 81
  8. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.sourceSum_fixedCenter_top line 85
  9. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.sourceSum_fixedCenter_comp line 107
  10. def OAI.Ostmann.Arithmetic.HistoryProductWindows.typeCenter line 128
  11. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.sourceSum_pruned_initial line 131
  12. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.sourceSum_extracted_pruned_initial line 148
  13. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.removedCenter_eq_typeCenter line 177
  14. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.inheritedCenter_eq_arrays line 185