Frobenius

Abstract

Frobenius.

Definition 1.1 (Unramified In).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/Frobenius.UnramifiedIn

Formalization. D5/S3/Factorization/Galois/Chebotarev/Frobenius.UnramifiedIn (✓ std3).

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

Commentary.

A prime of 𝓞 K is unramified in L if it is nonzero and every maximal prime above it is unramified over 𝓞 K.

Definition 1.2 (frobenius Class).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/Frobenius.frobeniusClass

Formalization. D5/S3/Factorization/Galois/Chebotarev/Frobenius.frobeniusClass (✓ std3).

Source. Repository-derived.

Commentary.

The Frobenius conjugacy class of a prime, with the trivial class as a default value.

Theorem 1.3 (Frobenius).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/Frobenius.exists_prime_dvd_natCast_mem

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

Commentary.

A prime ideal containing (n : 𝓞 K) for 1 < n contains a prime factor of n.

Truth anchor: D5/S3/Factorization/Galois/Chebotarev/Frobenius.UnramifiedIn
Truth anchor: D5/S3/Factorization/Galois/Chebotarev/Frobenius.exists_prime_dvd_natCast_mem
Truth anchor: D5/S3/Factorization/Galois/Chebotarev/Frobenius.frobeniusClass
Dependency: D5/S3/Analytic/Zeta/NumberField/Density