OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedRelabelExpr.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel line 13
  2. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_integerEval line 15
  3. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_rationalEval line 19
  4. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_denominator line 23
  5. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_valid line 27
  6. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_integralAt line 31
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_good line 35
  8. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_syntaxSize line 40
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_degreeBudget line 44
  10. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_fixedBound line 48
  11. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_fixedLogBound line 52
  12. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_supportModulus line 56
  13. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_numerator line 62
  14. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_totalDegree line 68
  15. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_comp line 73
  16. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_id line 77
  17. theorem OAI.Ostmann.Characters.TemplateOneSidedRelabel.relabel_numerator_ne_zero line 80