OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedPhasePriorJoinMasks.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.Template.OneSidedPhase.longCoordinateMask line 13
2. def OAI.Ostmann.Characters.Template.OneSidedPhase.shortCoordinateMask line 16
3. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.coordinateMaskProduct_twoPrimeAssignment line 18
4. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.norm_longCoordinateMask_le line 31
5. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.norm_shortCoordinateMask_le line 39
6. def OAI.Ostmann.Characters.Template.OneSidedPhase.coordinateMembershipMask line 42
7. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.norm_coordinateMembershipMask_le line 47