OAI/NumberTheory/Ostmann/Characters/TemplateCore.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Ostmann.Characters.Template.Role line 9
  2. structure OAI.Ostmann.Characters.Template.Layout line 16
  3. instance OAI.Ostmann.Characters.Template.(instance at line 22) line 22
  4. def OAI.Ostmann.Characters.Template.Layout.IsPivot line 24
  5. def OAI.Ostmann.Characters.Template.Layout.IsCopied line 26
  6. def OAI.Ostmann.Characters.Template.Layout.IsOutside line 30
  7. def OAI.Ostmann.Characters.Template.Layout.step line 32
  8. theorem OAI.Ostmann.Characters.Template.pivot_not_copied line 42
  9. theorem OAI.Ostmann.Characters.Template.word_copied line 51
  10. theorem OAI.Ostmann.Characters.Template.future_pivot_copied line 54
  11. theorem OAI.Ostmann.Characters.Template.future_anchor_outside line 58
  12. def OAI.Ostmann.Characters.Template.wordEquiv line 69
  13. def OAI.Ostmann.Characters.Template.futurePivotEquiv line 86
  14. def OAI.Ostmann.Characters.Template.futureAnchorEquiv line 109