OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedPhaseActual.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.Template.OneSidedPhase.differenceGraph line 13
2. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.differenceGraph_self line 18
3. def OAI.Ostmann.Characters.Template.OneSidedPhase.phasePair line 23
4. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.phasePair_oneSided line 33
5. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.phasePair_unary_norms line 55
6. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.exposedCharacter_apply line 70
7. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.phasePair_square line 77