Lean: bound |g(b)| for an integer polynomial via its 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 ℝ).