OAI/NumberTheory/Ostmann/Characters/TemplateGraphAnchors.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Characters.Template.Word line 9
  2. def OAI.Ostmann.Characters.Template.anchorCopied line 12
  3. def OAI.Ostmann.Characters.Template.freshAnchor line 17
  4. def OAI.Ostmann.Characters.Template.carryRetired line 29
  5. def OAI.Ostmann.Characters.Template.retiredAnchors line 34
  6. def OAI.Ostmann.Characters.Template.pathSigns line 42
  7. theorem OAI.Ostmann.Characters.Template.pathSigns_last line 47
  8. theorem OAI.Ostmann.Characters.Template.pathSigns_castSucc line 53
  9. theorem OAI.Ostmann.Characters.Template.rowSign_word_step line 58
  10. theorem OAI.Ostmann.Characters.Template.copyUnit_injective line 66
  11. theorem OAI.Ostmann.Characters.Template.pathSigns_injective line 70
  12. theorem OAI.Ostmann.Characters.Template.actual_code_final_injective line 90