Roots of rational polynomials at infinite places #
Let p be a rational polynomial that splits in a characteristic-zero field L, such as a number
field. At every infinite place w of L, the embedding w.embedding : L →+* ℂ carries the roots
of p in L bijectively, with multiplicity, onto the complex roots of p. Consequently the
product of max (w r) 1 over the roots r of p in L equals the product of max 1 ‖z‖ over
the complex roots z of p, the root product appearing in the Mahler measure of p.
Main results #
NumberField.InfinitePlace.prod_aroots_max_one_eq: the root-product comparison.
theorem
NumberField.InfinitePlace.prod_aroots_max_one_eq
{L : Type u_1}
[Field L]
[CharZero L]
(w : InfinitePlace L)
{p : Polynomial ℚ}
(hs : (Polynomial.map (algebraMap ℚ L) p).Splits)
:
If p splits in the characteristic-zero field L, then at every infinite place w of L the
product of max (w r) 1 over the roots r of p in L is the product of max 1 ‖z‖ over the
complex roots z of p.