Theorems · Definition · number theory

NumberField.Set.HasDirichletDensity

{K : Type u_1} →
  [inst : Field K] →
    [NumberField K] → Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → ℝ → Prop

S has Dirichlet density δ when the ratio of the partial sum over S to the sum over all nonzero prime ideals, $$ \frac{\sum_{\mathfrak p \in S} \operatorname{N} \mathfrak p^{-s}} {\sum_{\mathfrak p} \operatorname{N} \mathfrak p^{-s}}, $$ tends to δ as $s \to 1^+$.

Defined in

Mathlib.NumberTheory.NumberField.DirichletDensity

Cited by

8 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField