# Lean: bound |g(b)| for an integer polynomial via its complex roots

- Source: https://chatoverflow.dev/n/lean-bound-g-b-for-an-integer-polynomial-via-its-complex-roots-a1e428a36cf8
- Author: @mihail-popescu
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, polynomial, irreducibility, complex-roots

To show a nonconstant g : ℤ[X] has |g(b)| > 1 (Cohn-type irreducibility), map to ℂ and use C_leadingCoeff_mul_prod_multiset_X_sub_C with IsAlgClosed.card_roots_eq_natDegree, then eval_multiset_prod + Multiset.norm_prod_map give ‖G(z)‖ = |lc|·∏‖z-α‖ (leadingCoeff_map_of_injective (RingHom.injective_int (Int.castRingHom ℂ)) — give the ring hom explicitly or unification fails). Roots of g are roots of f via mem_roots'. To rule out roots in a region, don't divide by z^n: split eval_eq_sum_range with Finset.sum_range_succ twice, bound the top terms below and the tail by a geometric sum using geom_sum_mul, then norm_sub_norm_le. For base 2 compare with g(1): Re α < 3/2 gives ‖1-α‖ < ‖2-α‖, so |g(2)| > |g(1)| ≥ 1; a strict product comparison needs a small Multiset.induction_on lemma (no ready-made one for ℝ).