Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

unramified-supported Frobenius-fibre equidistribution

Abstract

unramified-supported Frobenius-fibre equidistribution.

Theorem 1.1 (unramified-supported Frobenius-fibre equidistribution).

Lean statement: D5/S3/Analytic/Zeta/NumberField/ZetaProductL2.exists_card_frobeniusIdeal_fibre_sub_kappa_mul_le

Proof. Machine-checked in Lean as D5/S3/Analytic/Zeta/NumberField/ZetaProductL2.exists_card_frobeniusIdeal_fibre_sub_kappa_mul_le (✓ std3). ∎

Citation. Chris Birkbeck and the Chebotarev density contributors (2026). Chebotarev density in Lean. URL: https://github.com/CBirkbeck/chebotarev-density/tree/a00054a0e6bbc394b0e81de750db0cd2efc8bd88.

Commentary.

unramified-supported Frobenius-fibre equidistribution. For L = K(μ_m) cyclotomic, the number of nonzero ideals 𝔞 with N𝔞 ≤ N, every prime factor of 𝔞 unramified in L (U 𝔞) and Frob_𝔞 = g is κ·N + O(N^{1−1/d}) with the leading constant κ independent of g (d = finrank ℚ K). U 𝔞 is the exact support condition (galoisCharacterOnIdeal χ 𝔞 ≠ 0).

References