OAI/NumberTheory/Ostmann/Characters/TemplateSchedule.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Ostmann.Characters.Template.InitialRole line 9
  2. def OAI.Ostmann.Characters.Template.InitialRole.role line 16
  3. def OAI.Ostmann.Characters.Template.initial line 22
  4. def OAI.Ostmann.Characters.Template.schedule line 28
  5. theorem OAI.Ostmann.Characters.Template.initial_word_unique line 32
  6. def OAI.Ostmann.Characters.Template.wordPathEquiv line 42
  7. theorem OAI.Ostmann.Characters.Template.active_word_card line 53
  8. theorem OAI.Ostmann.Characters.Template.initial_pivot_unique line 57
  9. def OAI.Ostmann.Characters.Template.pivotEquiv line 73
  10. def OAI.Ostmann.Characters.Template.pivotSlot line 83
  11. theorem OAI.Ostmann.Characters.Template.pivotSlot_unique line 86
  12. theorem OAI.Ostmann.Characters.Template.initial_anchor_unique line 91
  13. def OAI.Ostmann.Characters.Template.anchorEquiv line 109
  14. def OAI.Ostmann.Characters.Template.anchorSlot line 119