Coefficient-height bounds for polynomial values

theorem NairTenenbaum.coeff_natAbs_le_height (Q : Polynomial ℤ) (i : ℕ) : (Q.coeff i).natAbs ≤ polynomialHeight Q

theorem NairTenenbaum.polynomialHeight_pos {Q : Polynomial ℤ} (hQ : Q ≠ 0) : 0 < polynomialHeight Q

theorem NairTenenbaum.one_le_polynomialHeight {Q : Polynomial ℤ} (hQ : Q ≠ 0) : 1 ≤ ↑(polynomialHeight Q)

A nonzero integral polynomial has real coefficient height at least one.

theorem NairTenenbaum.eval_natAbs_le_height (Q : Polynomial ℤ) (n : ℤ) : (Polynomial.eval n Q).natAbs ≤ polynomialHeight Q * (Q.natDegree + 1) * max 1 n.natAbs ^ Q.natDegree

A coefficient-uniform bound on integral polynomial values.