Theorems · Theorem · number theory

Polynomial.cyclotomic_dvd_of_mahlerMeasure_eq_one

∀ {p : Polynomial ℤ},
  (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 →
    ¬Polynomial.X ∣ p → p.degree ≠ 0 → ∃ n, 0 < n ∧ Polynomial.cyclotomic n ℤ ∣ p

If an integer non-constant polynomial has Mahler measure equal to 1 and is not a multiple of X, then it is divisible by a cyclotomic polynomial.

Defined in

Mathlib.NumberTheory.MahlerMeasure

Cited by

0 results in Mathlib

Foundations

Depth 304 from the axioms · uses propext, Classical.choice, Quot.sound