OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedCancellationFrequencySupport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.historyFrequencyBounds line 13
  2. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.historyFrequencyBounds_root line 19
  3. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.frequencyArithmetic line 25
  4. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.outsideHistorySupport line 36
  5. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.sampledHistoryArithmetic_split line 47
  6. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.historyResidueGuards line 58
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.pivotExpression_good_of_nodeArithmetic line 67
  8. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.rootResidueGuards_iff_arithmetic line 77
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.historyResidueGuards_holds line 85