[proofplan] We show that if $n \cdot z = 0$ in $A \otimes_\mathbb{Z} B$ for some $n \in \mathbb{N}$ and $z \in A \otimes_\mathbb{Z} B$, then $z = 0$. Writing $z = \sum_{i=1}^\ell a_i \otimes b_i$, the [Finite Generation of Zero Relations](/theorems/2910) theorem lets us pass from the potentially enormous tensor product $A \otimes_\mathbb{Z} B$ to a tensor product of finitely generated subgroups $A' \otimes_\mathbb{Z} B'$. Since $A$ and $B$ are torsion-free, these finitely generated subgroups are free abelian by the classification theorem, so $A' \otimes_\mathbb{Z} B' \cong \mathbb{Z}^{k\ell}$ is itself torsion-free, and the vanishing of $n \cdot z$ forces $z = 0$. [/proofplan] [step:Reduce to a tensor product of finitely generated subgroups] Suppose $z \in A \otimes_\mathbb{Z} B$ satisfies $n \cdot z = 0$ for some $n \in \mathbb{N}$. Write $z = \sum_{i=1}^\ell a_i \otimes b_i$ for elements $a_i \in A$ and $b_i \in B$. Then \begin{align*} n \cdot z = \sum_{i=1}^\ell (n a_i) \otimes b_i = 0 \end{align*} in $A \otimes_\mathbb{Z} B$. By the [Finite Generation of Zero Relations](/theorems/2910) theorem applied to $\sum_{i=1}^\ell (na_i) \otimes b_i = 0$, there exist finitely generated subgroups $A_0 \subseteq A$ and $B_0 \subseteq B$ containing all the $na_i$ and $b_i$ respectively, such that $\sum_{i=1}^\ell (na_i) \otimes b_i = 0$ already holds in $A_0 \otimes_\mathbb{Z} B_0$. Define $A' \subseteq A$ to be the subgroup generated by $A_0$ and $\{a_1, \ldots, a_\ell\}$, and $B' = B_0$. Then $A'$ and $B'$ are finitely generated subgroups of $A$ and $B$ respectively, containing all $a_i$ and $b_i$. The element $z = \sum_{i=1}^\ell a_i \otimes b_i$ is well-defined in $A' \otimes_\mathbb{Z} B'$, and $n \cdot z = \sum_{i=1}^\ell (na_i) \otimes b_i = 0$ in $A' \otimes_\mathbb{Z} B'$ (since $na_i \in A_0 \subseteq A'$ and $b_i \in B_0 = B'$, and the relation already holds in $A_0 \otimes_\mathbb{Z} B_0$, hence also in the larger $A' \otimes_\mathbb{Z} B'$). [guided] We want to show $z = 0$, given that $n \cdot z = 0$. The difficulty is that $A \otimes_\mathbb{Z} B$ may be enormous and hard to work with directly. The strategy is to confine the problem to a finitely generated setting where we have structural theorems. Write $z = \sum_{i=1}^\ell a_i \otimes b_i$. Then $n \cdot z = \sum_{i=1}^\ell (na_i) \otimes b_i = 0$ in $A \otimes_\mathbb{Z} B$, using the $\mathbb{Z}$-bilinearity of the tensor product (specifically, $n \cdot (a \otimes b) = (na) \otimes b$). Now we apply the [Finite Generation of Zero Relations](/theorems/2910) theorem. This theorem states: if $\sum_i m_i \otimes n_i = 0$ in $M \otimes_R N$, then there exist finitely generated submodules $M' \subseteq M$, $N' \subseteq N$ containing all the $m_i$ and $n_i$ such that the relation already holds in $M' \otimes_R N'$. We apply this with $M = A$, $N = B$, $R = \mathbb{Z}$, $m_i = na_i$, $n_i = b_i$. We obtain finitely generated subgroups $A_0 \subseteq A$ (containing all $na_i$) and $B_0 \subseteq B$ (containing all $b_i$) with $\sum_i (na_i) \otimes b_i = 0$ in $A_0 \otimes_\mathbb{Z} B_0$. We enlarge $A_0$ to $A' := \langle A_0, a_1, \ldots, a_\ell \rangle$ so that the element $z = \sum_i a_i \otimes b_i$ is defined in $A' \otimes_\mathbb{Z} B'$ (with $B' = B_0$). Since $A_0 \subseteq A'$, the canonical map $A_0 \otimes_\mathbb{Z} B_0 \to A' \otimes_\mathbb{Z} B'$ sends the relation $\sum_i (na_i) \otimes b_i = 0$ to the same relation in $A' \otimes_\mathbb{Z} B'$. [/guided] [/step] [step:Apply the structure theorem to identify $A' \otimes_\mathbb{Z} B'$ with a free abelian group] Since $A$ is a torsion-free abelian group and $A'$ is a finitely generated subgroup of $A$, the group $A'$ is a finitely generated torsion-free abelian group. By the [Structure Theorem for Finitely Generated Abelian Groups](/theorems/???), $A' \cong \mathbb{Z}^k$ for some $k \geq 0$ (the torsion part is absent because $A'$ is torsion-free). Similarly, $B' \cong \mathbb{Z}^j$ for some $j \geq 0$. By the [distributivity of tensor products over direct sums](/theorems/2827) and the [unit isomorphism](/theorems/2827) $\mathbb{Z} \otimes_\mathbb{Z} \mathbb{Z} \cong \mathbb{Z}$, we have \begin{align*} A' \otimes_\mathbb{Z} B' \cong \mathbb{Z}^k \otimes_\mathbb{Z} \mathbb{Z}^j \cong \bigoplus_{i=1}^k \bigoplus_{i'=1}^j (\mathbb{Z} \otimes_\mathbb{Z} \mathbb{Z}) \cong \mathbb{Z}^{kj}. \end{align*} In particular, $A' \otimes_\mathbb{Z} B'$ is a free abelian group, and therefore torsion-free. [guided] Why does the structure theorem give a purely free group? A finitely generated abelian group decomposes as $\mathbb{Z}^r \oplus \mathbb{Z}/d_1\mathbb{Z} \oplus \cdots \oplus \mathbb{Z}/d_s\mathbb{Z}$. But $A'$ is a subgroup of the torsion-free group $A$: if $a' \in A'$ satisfies $d \cdot a' = 0$ for some $d \geq 1$, then $a' = 0$ because $A$ has no torsion. So $A'$ is torsion-free, meaning $s = 0$ and $A' \cong \mathbb{Z}^k$. The same argument gives $B' \cong \mathbb{Z}^j$. Now we compute $A' \otimes_\mathbb{Z} B'$. By the [Structural Isomorphisms of Tensor Products](/theorems/2827), the tensor product distributes over direct sums: \begin{align*} \mathbb{Z}^k \otimes_\mathbb{Z} \mathbb{Z}^j \cong \left(\bigoplus_{i=1}^k \mathbb{Z}\right) \otimes_\mathbb{Z} \mathbb{Z}^j \cong \bigoplus_{i=1}^k (\mathbb{Z} \otimes_\mathbb{Z} \mathbb{Z}^j) \cong \bigoplus_{i=1}^k \bigoplus_{i'=1}^j (\mathbb{Z} \otimes_\mathbb{Z} \mathbb{Z}). \end{align*} The unit isomorphism $\mathbb{Z} \otimes_\mathbb{Z} \mathbb{Z} \cong \mathbb{Z}$ (via $a \otimes b \mapsto ab$) gives $A' \otimes_\mathbb{Z} B' \cong \mathbb{Z}^{kj}$, which is a free abelian group and hence torsion-free: if $n \cdot v = 0$ in $\mathbb{Z}^{kj}$ with $n \geq 1$, then $v = 0$. [/guided] [/step] [step:Conclude that $z = 0$ in $A \otimes_\mathbb{Z} B$] We have $n \cdot z = 0$ in $A' \otimes_\mathbb{Z} B' \cong \mathbb{Z}^{kj}$, and $\mathbb{Z}^{kj}$ is torsion-free. Therefore $z = 0$ in $A' \otimes_\mathbb{Z} B'$. The inclusion maps $\iota_A: A' \hookrightarrow A$ and $\iota_B: B' \hookrightarrow B$ induce an $R$-module homomorphism $\iota_A \otimes \iota_B: A' \otimes_\mathbb{Z} B' \to A \otimes_\mathbb{Z} B$ by the [Tensor Product of Homomorphisms](/theorems/2912). The element $z = \sum_{i=1}^\ell a_i \otimes b_i$ in $A \otimes_\mathbb{Z} B$ is the image of $\sum_{i=1}^\ell a_i \otimes b_i$ in $A' \otimes_\mathbb{Z} B'$ under this map. Since $z = 0$ in $A' \otimes_\mathbb{Z} B'$, its image $(\iota_A \otimes \iota_B)(z) = 0$ in $A \otimes_\mathbb{Z} B$. Since $z \in A \otimes_\mathbb{Z} B$ was an arbitrary element with $nz = 0$ for some $n \in \mathbb{N}$, the tensor product $A \otimes_\mathbb{Z} B$ is torsion-free. [/step]