Theorems · Theorem · number theory

Polynomial.pow_eq_one_of_mahlerMeasure_eq_one

∀ {p : Polynomial ℤ},
  (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 → ∀ {z : ℂ}, z ≠ 0 → z ∈ p.aroots ℂ → ∃ n, 0 < n ∧ z ^ n = 1

If an integer polynomial has Mahler measure equal to 1, then all its complex nonzero roots are roots of unity.

Defined in

Mathlib.NumberTheory.MahlerMeasure

Cited by

1 results in Mathlib

Foundations

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