Chebotarev Density Theorem

Abstract

Chebotarev Density Theorem.

Theorem 1.1 (Chebotarev Density Theorem).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/Main.chebotarev_density

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/Chebotarev/Main.chebotarev_density (✓ std3). ∎

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

Commentary.

For a finite Galois extension L/K of number fields and any conjugacy class C in Gal(L/K), the unramified prime ideals of K whose Frobenius class is C have Dirichlet density |C| / |Gal(L/K)|.

References

• Truth anchor: D5/S3/Factorization/Galois/Chebotarev/Main.chebotarev_density
• Dependency: D5/S3/Factorization/Galois/Chebotarev/Abelian
• Dependency: D5/S3/Factorization/Galois/Chebotarev/FixedFieldDensity