OAI/NumberTheory/Ostmann/Characters/TemplateHistoryUnaryBasic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.Template.unaryPivotColumn line 13
  2. def OAI.Ostmann.Characters.Template.unaryChildFrequency line 16
  3. def OAI.Ostmann.Characters.Template.unaryChildTree line 19
  4. def OAI.Ostmann.Characters.Template.historyUnary line 22
  5. def OAI.Ostmann.Characters.Template.historyRegularKappa line 34
  6. def OAI.Ostmann.Characters.Template.HistoryFrequencyUnits line 43
  7. theorem OAI.Ostmann.Characters.Template.HistoryFrequencyUnits.root line 48
  8. theorem OAI.Ostmann.Characters.Template.HistoryFrequencyUnits.child line 54
  9. theorem OAI.Ostmann.Characters.Template.historyFrequencyUnits_of_range line 61
  10. def OAI.Ostmann.Characters.Template.supportedHistoryUnary line 69