Theorems · Definition · number theory

NumberField.Set.dirichletDensity

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

The Dirichlet density of S as a real number, taking the junk value 0 when S has no density. As with tsum, this value only has content when S has a density; the genuine statement that S has density 0 is HasDirichletDensity S 0.

Defined in

Mathlib.NumberTheory.NumberField.DirichletDensity

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldNumberField