Theorems · Theorem · number theory

NumberField.Set.dirichletDensity_eq_zero_of_not_hasDirichletDensity

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))},
  (∀ (δ : ℝ), ¬NumberField.Set.HasDirichletDensity S δ) → NumberField.Set.dirichletDensity S = 0

If S has no Dirichlet density, then dirichletDensity S = 0.

Defined in

Mathlib.NumberTheory.NumberField.DirichletDensity

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldNumberField