OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedSourceScalesBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.TemplateOneSidedSourceScales.scaleStep line 10
2. def OAI.Ostmann.Characters.TemplateOneSidedSourceScales.scaleCount line 11
3. def OAI.Ostmann.Characters.TemplateOneSidedSourceScales.lowerExponent line 12
4. def OAI.Ostmann.Characters.TemplateOneSidedSourceScales.shortExponent line 13
5. def OAI.Ostmann.Characters.TemplateOneSidedSourceScales.longExponent line 14
6. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceScales.scale_exponents line 16
7. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceScales.exists_grid_of_gap line 28