OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedCancellationCrossData.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.conjugateProfile line 11
  2. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.conjugateProfile_eval line 15
  3. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.conjugateProfile_bound line 23
  4. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.conjugateData line 26
  5. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.multiplyData line 29
  6. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.conjugateData_weight line 39
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.multiplyData_weight line 46
  8. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.conjugateData_ranges line 60
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.ranges_mono_bound line 66
  10. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.multiplyData_ranges line 72