OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedPairwise.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.Template.OneSidedPhase.fixedPrimeSupport line 14
2. def OAI.Ostmann.Characters.Template.OneSidedPhase.unaryPrimeSupport line 17
3. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.twoPrimeAssignment_pairwise_iff line 20
4. def OAI.Ostmann.Characters.Template.OneSidedPhase.longPrimeSupportMask line 69
5. def OAI.Ostmann.Characters.Template.OneSidedPhase.shortPrimeSupportMask line 72
6. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.twoPrimeAssignment_support_indicator line 75
7. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.twoPrimeAssignment_support_indicator_of_coprime line 87
8. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.longPrimeSupportMask_norm_le line 94
9. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.shortPrimeSupportMask_norm_le line 97