OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedWindowRegularityBasic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.substitute_good line 14
  2. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.coordinateWindowExpressions_good line 21
  3. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.candidateWindowGuards_good line 31
  4. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.coordinateWindowGuards line 41
  5. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.coordinateWindowGuards_good line 45
  6. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.coordinateWindowGuards_length line 51
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.coordinateWindowGuards_size line 57
  8. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.positiveGuards_good line 63
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.nodeGuards_good line 70