OAI/NumberTheory/DirichletL/Moments/NaturalFixedRaySourceCharacters.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.relativeCharacter line 20
2. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.relativeCharacter_ideal line 23
3. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.relativeCharacter_norm line 28
4. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.relativeCharacter_modulus line 31
5. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.relativeCharacter_fixedQ line 35
6. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.excluded_product_ideal line 39
7. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.sector_element line 44
8. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.sector_fixedQ_iff line 52
9. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.sector_nonprincipal line 65