OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedCancellationLongData.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.longRatioData line 10
2. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.longRatioData_support line 18
3. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.longRatioData_weight line 25
4. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.longRatioData_ranges line 34
5. def OAI.Ostmann.Characters.TemplateOneSidedCancellation.crossHistoryData line 49
6. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.crossHistoryData_weight line 53
7. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.crossHistoryData_ranges line 63