OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedWindowRegularity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.historyGuards_good line 15
2. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.historyCoordinateWindowGuards_good line 56
3. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.bottomExpressions_good_of_frequencyArithmetic line 67
4. theorem OAI.Ostmann.Characters.TemplateOneSidedCancellation.indexedBottomExpressions_period_good_of_frequencyArithmetic line 96