Theorems · Theorem · number theory

NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (C : ClassGroup (NumberField.RingOfIntegers K)),
  Filter.Tendsto (fun s => ↑(Nat.card { I // ↑(Ideal.absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C }) / s) Filter.atTop
    (nhds
      (2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
          NumberField.Units.regulator K /
        (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|)))

The limit of the number of nonzero integral ideals of norm ≤ s in a fixed class C of the class group divided by s when s → +∞.

Defined in

Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField