OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedPhaseUnitsBasic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.Template.OneSidedPhase.extendUnitData line 14
  2. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.extendUnitData_prime line 17
  3. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.norm_extendUnitData line 21
  4. def OAI.Ostmann.Characters.Template.OneSidedPhase.pairedUnitUnary line 30
  5. def OAI.Ostmann.Characters.Template.OneSidedPhase.longUnitFactor line 33
  6. def OAI.Ostmann.Characters.Template.OneSidedPhase.shortUnitFactor line 37
  7. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.pairedUnitProduct_split line 40
  8. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.norm_longUnitFactor line 54
  9. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.norm_shortUnitFactor line 60
  10. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.longUnitFactor_twoPrimeAssignment line 64