I learned this through Ken Brown's textbook "Cohomology of Groups" (and studying under him): I basically use the beginning of his Chapter 5 and solve the two exercises in that section.

Let $M$ (resp. $M'$) be an arbitrary $G$-module (resp. $G'$-module), let $F$ (resp. $F'$) be a projective resolution of $\mathbb{Z}$ over $\mathbb{Z}G$ (resp. $\mathbb{Z}G'$), and consider the map $(F\otimes_GM)\otimes(F'\otimes_{G'}M')\rightarrow (F\otimes F')\otimes_{G\times G'}(M\otimes M')$ given by $(x\otimes m)\otimes(x'\otimes m')\mapsto(x\otimes x')\otimes(m\otimes m')$.

Note that $(F\otimes_GM)$ $\otimes(F'\otimes_{G'}M')$ = $(F\otimes M)_G \otimes(F'\otimes M')_G$ ,

which is the quotient of $F\otimes M\otimes F'\otimes M'$ by the subgroup generated by elements of the form $gx\otimes gm\otimes g'x'\otimes m'$. The isomorphism $F\otimes M\stackrel{\cong}{\rightarrow}M\otimes F$ of chain complexes ($M$ in dimension $0$) is given by $x\otimes m\mapsto (-1)^{deg(m)\cdot deg(x)}m\otimes x=m\otimes x$, and so the aforementioned quotient is isomorphic to $F\otimes F'\otimes M\otimes M'$ modulo the subgroup generated by elements of the form $(gx\otimes g'x'\otimes gm\otimes g'm')=(g,g')\cdot(x\otimes x'\otimes m\otimes m')$ where this latter action is the diagonal $(G\times G')$-action. Now this is precisely

$$(F\otimes F'\otimes M\otimes M')_{G\times G'} = (F\otimes F')\otimes_{G\times G'}(M\otimes M')$$ and hence the considered map is an isomorphism.

Assuming now that either $M$ or $M'$ is $\mathbb{Z}$-free, we have a corresponding Künneth formula $\bigoplus_{p=0}^nH_p(G,M)\otimes H_{n-p}(G',M')\rightarrow H_n(G\times G',M\otimes M')$

$\rightarrow\bigoplus_{p=0}^{n-1}Tor_1^\mathbb{Z}(H_p(G,M),H_{n-p-1}(G',M'))$ by Proposition I.0.8[Brown]. Note that in order to apply the proposition we needed one of the chain complexes (say, $F\otimes_G M$) to be dimension-wise $\mathbb{Z}$-free (and so with a free resolution $F$ this means we needed $M$ to be $\mathbb{Z}$-free).

Actually, the general Künneth theorem has a more relaxed condition and it suffices to choose $M$ (or $M'$) as a $\mathbb{Z}$-torsion-free module}.

Cohomology Künneth Formula (no proofs, just statements/notes)

Let $M$ (resp. $M'$) be an arbitrary $G$-module (resp. $G'$-module), let $F$ (resp. $F'$) be a projective resolution of $\mathbb{Z}$ over $\mathbb{Z}G$ (resp. $\mathbb{Z}G'$), and consider the cochain cross-product $Hom_G(F,M)\otimes Hom_{G'}(F',M')\rightarrow Hom_{G\times G'}(F\otimes F',M\otimes M')$ which maps the cochains $u$ and $u'$ to $u\times u'$ given by $\langle u\times u',x\otimes x'\rangle=(-1)^{deg(u')\cdot deg(x)}\langle u,x\rangle\otimes\langle u',x'\rangle$. This map is an isomorphism under the hypothesis that either $H_i(G,M)$ or $H_i(G',M')$ is of finite type, that is, the $i$th-homology group is finitely generated for all $i$ (alternatively, we could simply require the projective resolution $F$ or $F'$ to be finitely generated).

For example, if $M=\mathbb{Z}$ then $Hom_G(-,\mathbb{Z})$ commutes with finite direct sums, so we need only consider the case $F=\mathbb{Z}G$. An inverse to the above map is given by $t\mapsto \varepsilon\otimes \phi$, where $\varepsilon$ is the augmentation map and $\phi:F'\rightarrow M'$ is given by $\phi(f')=t(1\otimes f')$. Note that this does not hold for infinitely generated $P=\bigoplus^\infty \mathbb{Z}G$ because $Hom_G(P,\mathbb{Z})\cong\prod^\infty \mathbb{Z}$ is not $\mathbb{Z}$-projective (i.e. free abelian).

Assuming now that either $M$ or $M'$ is $\mathbb{Z}$-free, we have a corresponding Künneth formula $\bigoplus_{p=0}^nH^p(G,M)\otimes H^{n-p}(G',M')\rightarrow H^n(G\times G',M\otimes M')\rightarrow$

$\bigoplus_{p=0}^{n+1}Tor_1^\mathbb{Z}(H^p(G,M),H^{n-p+1}(G',M'))$ by Proposition I.0.8[Brown].

`$G_1$`

and`$G_2$`

are finite groups, then there is what is called a Tor spectral sequence, which requires contributions from the higher Tor groups over $M$ and is, unfortunately, not quite as simple as all of the Tor groups appearing in a direct sum. If the coefficient actions are not trivial then it gets more complicated. $\endgroup$ – Tyler Lawson Sep 15 '11 at 2:14