OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedRelabelGuards.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabelGuard line 13
  2. def OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabelResidueGuard line 16
  3. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabelGuard_holds line 19
  4. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabelResidueGuard_holds line 23
  5. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabelResidueGuard_modulus line 28
  6. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.residueModulus_relabel line 32
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.rootResidueGuards_relabel line 36
  8. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.nodeResidueGuards_relabel line 42
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.historyResidueGuards_relabel line 49
  10. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.historyResidueModulus_relabel line 58
  11. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.substituteGuard_relabel line 64
  12. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.substituteGuard_relabelExpressions line 69
  13. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.positiveGuards_relabel line 74
  14. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.nodeGuards_relabel line 80
  15. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.historyGuards_relabel line 87
  16. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.maskGuards_relabel line 99
  17. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.coreGuardList_relabel line 110