Theorems · Theorem · number theory

Polynomial.isIntegral_of_mahlerMeasure_eq_one

∀ {p : Polynomial ℤ},
  (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 → ∀ {z : ℂ}, z ∈ p.aroots ℂ → IsIntegral ℤ z

If an integer polynomial has Mahler measure equal to 1, then all its complex roots are integral over ℤ.

Defined in

Mathlib.NumberTheory.MahlerMeasure

Cited by

2 results in Mathlib

Foundations

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