OAI/NumberTheory/DirichletL/RayQuotient.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.RayQuotient.Characters line 13
  2. abbrev OAI.SevenEighths.RayQuotient.classNumber line 14
  3. theorem OAI.SevenEighths.RayQuotient.classNumber_pos line 16
  4. theorem OAI.SevenEighths.RayQuotient.character_unitInvariant line 20
  5. def OAI.SevenEighths.RayQuotient.toFullRay line 25
  6. theorem OAI.SevenEighths.RayQuotient.toFullRay_injective line 30
  7. theorem OAI.SevenEighths.RayQuotient.toFullRay_eq_one line 34
  8. def OAI.SevenEighths.RayQuotient.idealCharacter line 41
  9. theorem OAI.SevenEighths.RayQuotient.idealCharacter_eq_fullRay line 44
  10. def OAI.SevenEighths.RayQuotient.identityClass line 47
  11. theorem OAI.SevenEighths.RayQuotient.identityClass_iff_generator line 52
  12. theorem OAI.SevenEighths.RayQuotient.norm_idealCharacter_le_one line 74
  13. theorem OAI.SevenEighths.RayQuotient.idealCharacter_one line 78
  14. theorem OAI.SevenEighths.RayQuotient.sum_idealCharacters line 83
  15. theorem OAI.SevenEighths.RayQuotient.average_idealCharacters line 94
  16. theorem OAI.SevenEighths.RayQuotient.identityClass_globalUnits line 102