OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedCancellationGuards.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.Guard.realHolds line 10
  2. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.Guard.realHolds_iff line 15
  3. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.guardPolynomials line 30
  4. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.polynomialSupport_iff_realGuards line 33
  5. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.polynomialSupport_iff_guards line 43
  6. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.windowGuards line 54
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.windowGuards_holds line 59
  8. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.binGuards line 66
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.binGuards_holds_iff line 69