The unramified primes carry all of the density

Let L / K be an extension of number fields. The primes of 𝓞 K ramified in L form the finite set ramifiedPrimes K L, so their complement has Dirichlet density 1.

Main results

• NumberField.Chebotarev.hasDirichletDensity_compl_ramifiedPrimes: the primes outside the finite ramified set have Dirichlet density 1.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.

theorem NumberField.Chebotarev.hasDirichletDensity_compl_ramifiedPrimes (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Set.HasDirichletDensity (↑(ramifiedPrimes K L))ᶜ 1

The unramified primes have density one. Only finitely many primes of 𝓞 K ramify in L, so they carry density 0 and their complement carries all of it.