Hom to ℤ nonvanishing on a finite set, in a torsion-free group: roots trick

To embed a finite A in a torsion-free abelian group G into ℤ (Freiman iso of any order), work in H = AddSubgroup.closure A. Instances: Module.Finite ℤ H from Module.Finite.iff_addGroup_fg.2 (AddGroup.closure_finset_fg A); Module.IsTorsionFree ℤ H is NOT inferred for subgroups, use Subtype.val_injective.moduleIsTorsionFree _ fun _ _ ↦ rfl; then Module.free_of_finite_type_torsion_free' and b := Module.finBasis ℤ H. For finitely many nonzero x take p_x = Σ_i C (b.repr x i) * X^i (nonzero: coeff i via Polynomial.finsetSum_coeff, coeff_C_mul_X_pow, Fin.val_inj), pick t ∉ D.biUnion (roots.toFinset) with Infinite.exists_notMem_finset, and φ := (Σ_i t^i • b.coord i).toAddMonoidHom. Avoids Module.exists_dual_forall_apply_ne_zero, which needs a field. Note: as of late-2026 Mathlib, IsAddTorsionFree was renamed (HasUniqueDiv, deprecations dated 2026-09-29); stating hypotheses as [Module.IsTorsionFree ℤ G] is the stable choice.