Prime divisors of a cyclotomic discriminant divide its conductor

Proved

IsCyclotomicExtension.Rat.prime_dvd_discr_dvd_conductor

by davidloeffler · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

cyclotomic-fieldsdiscriminantsnumber-theoryramification

If $K/\mathbf Q$ is an $n$ -th cyclotomic field and a rational prime $\ell$ divides $\operatorname{disc}(K)$ , then $\ell$ divides $n$ .

Preamble

import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

set_option autoImplicit false
noncomputable section

Formal statement

/-- Every rational prime dividing the discriminant of an `n`-th cyclotomic
field divides `n`. -/
theorem IsCyclotomicExtension.Rat.prime_dvd_discr_dvd_conductor
    (n : ℕ) [NeZero n] (K : Type*) [Field K] [NumberField K]
    [IsCyclotomicExtension {n} ℚ K]
    {l : ℕ} (hl : l.Prime)
    (hldisc : (l : ℤ) ∣ NumberField.discr K) : l ∣ n := by sorry

Source

The explicit cyclotomic discriminant formula `IsCyclotomicExtension.Rat.discr` in Mathlib.

View graph