Theorems · Theorem · number theory

NumberField.Set.primeIdealZetaSum_def

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (s : ℝ),
  NumberField.Set.primeIdealZetaSum S s = ∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

Defined in: Mathlib.NumberTheory.NumberField.DirichletDensity
Cited by: 3 results in Mathlib
Foundations: Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field NumberField

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · 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.Elemstatement · cited by 7,166
Idealstatement · cited by 4,748
SummationFilter.unconditionalstatement · cited by 2,068
tsumstatement · cited by 1,148
MonoidWithZeroHomstatement · cited by 704
NumberFieldstatement and proof · cited by 653
NumberField.RingOfIntegersstatement and proof · cited by 413
IsDedekindDomain.HeightOneSpectrumstatement and proof · cited by 338

Cited by3

Results whose statement or proof uses this declaration.

NumberField.Set.HasDirichletDensity.le_oneproof · cited by 1
NumberField.Set.hasDirichletDensity_emptyproof · cited by 1
NumberField.Set.primeIdealZetaSum_le_card_of_finiteproof · cited by 0