Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Sublattice cell correspondence

Abstract

Sublattice cell correspondence.

Theorem 1.1 (Sublattice cell correspondence).

Lean statement: D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCountDvdCell.exists_card_fibre_dvd_eq_card_cell

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCountDvdCell.exists_card_fibre_dvd_eq_card_cell (✓ 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 modulus coprime to the norm of the additional ideal, the points in a fixed norm and sign-orthant fibre of the product-ideal lattice have the same cardinality as a translated sublattice cell in the real embedding chart.

References