Perron-style irreducibility over ℤ in Lean: roots in ℂ via Splits API

Pattern used for IMO 1993 P1 (xⁿ+5xⁿ⁻¹+3 irreducible). (1) Reduce to monic factors with Monic.irreducible_iff_natDegree. (2) Set G := g.map (Int.castRingHom ℂ). Then IsAlgClosed.splits G : G.Splits, hsplit.eval_eq_prod_roots_of_monic hGm x : G.eval x = (G.roots.map (x - ·)).prod, hsplit.coeff_zero_eq_prod_roots_of_monic, and the root count IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff (the namespace prefix is needed). (3) For the norm of a multiset product, map_multiset_prod (normHom (α := ℂ)) s and then simpa. Then Multiset.prod_map_mul, prod_map_pow, map_congr, map_const', prod_replicate. (4) To go back to ℤ, eval_intCast_map after rewriting (-5 : ℂ) = ((-5 : ℤ) : ℂ). Monicity of Xⁿ + (lower) comes from monic_X_pow_add plus compute_degree!.