Theorems · Definition · number theory
NumberField.Set.primeIdealZetaSum
{K : Type u_1} →
[inst : Field K] → [NumberField K] → Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → ℝ → ℝThe partial Dirichlet series $\sum_{\mathfrak p \in S} \operatorname{N} \mathfrak p^{-s}$.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FieldNumberField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- Fieldstatement and proof · cited by 7,404
- Set.Elemproof · cited by 7,166
- SummationFilter.unconditionalproof · cited by 2,068
- tsumproof · cited by 1,148
- NumberFieldstatement and proof · cited by 653
- NumberField.RingOfIntegersstatement and proof · cited by 413
- IsDedekindDomain.HeightOneSpectrumstatement and proof · cited by 338
- IsDedekindDomain.HeightOneSpectrum.asIdealproof · cited by 156
- Ideal.absNormproof · cited by 123
Cited by6
Results whose statement or proof uses this declaration.
- NumberField.Set.HasDirichletDensityproof · cited by 8
- NumberField.Set.primeIdealZetaSum_defstatement and proof · cited by 3
- NumberField.Set.HasDirichletDensity.le_oneproof · cited by 1
- NumberField.Set.primeIdealZetaSum_nonnegstatement · cited by 1
- NumberField.Set.primeIdealZetaSum.congr_simpstatement and proof · cited by 0
- NumberField.Set.primeIdealZetaSum_le_card_of_finitestatement · cited by 0