OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedCancellationSurvivingModulusBasic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.TemplateOneSidedBudget.SameResidueModuli line 14
  2. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.sameResidueModuli_refl line 17
  3. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.expressionProduct_sameResidueModuli line 19
  4. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.finiteProductExpression_sameResidueModuli line 33
  5. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.copiedExpression_sameResidueModuli line 42
  6. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.pivotExpression_sameResidueModuli line 48
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.childExpressions_sameResidueModuli line 57
  8. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.residueGuard_modulus_congr line 67
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.rootResidueGuards_moduli_congr line 72
  10. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.nodeResidueGuards_moduli_congr line 82
  11. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.historyResidueGuards_moduli_congr line 92
  12. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.historyResidueModulus_congr line 107