[proofplan] Two assertions: $\rho \otimes \rho'$ is a representation of $G$, and its character is the pointwise product $\chi_\rho \chi_{\rho'}$. The homomorphism property follows from the bilinearity of $\otimes$: applying $\rho \otimes \rho'$ to a pure tensor commutes with $\otimes$, so $(\rho \otimes \rho')(g_1)(\rho \otimes \rho')(g_2) = (\rho \otimes \rho')(g_1 g_2)$ on pure tensors, and linearity extends this to all of $V \otimes V'$. For the character formula, we simultaneously diagonalise $\rho(g)$ on $V$ and $\rho'(g)$ on $V'$ — possible because each operator has finite order — and observe that the basis of pure tensor products $v_i \otimes w_j$ diagonalises $(\rho \otimes \rho')(g)$ with eigenvalues $\lambda_i \mu_j$. Summing, \begin{align*} \chi_{\rho \otimes \rho'}(g) = \sum_{i,j} \lambda_i \mu_j = \biggl(\sum_i \lambda_i\biggr)\biggl(\sum_j \mu_j\biggr) = \chi_\rho(g)\, \chi_{\rho'}(g). \end{align*} [/proofplan] [step:Verify $\rho \otimes \rho'$ is a representation by checking the homomorphism property on pure tensors] The defining formula for $(\rho \otimes \rho')(g)$ specifies its action on a general element $\sum \lambda_{ij}\, v_i \otimes w_j$ of $V \otimes V'$ by linearly extending the rule \begin{align*} (\rho \otimes \rho')(g)(v \otimes w) := (\rho(g)v) \otimes (\rho'(g)w). \end{align*} This rule is well-defined as a linear map on $V \otimes V'$ because the right-hand side is bilinear in $(v, w)$: bilinearity in $v$ uses linearity of $\rho(g)$ and bilinearity of $\otimes$, and similarly in $w$. By the universal property of the tensor product, the bilinear map $(v, w) \mapsto \rho(g)v \otimes \rho'(g)w$ from $V \times V'$ to $V \otimes V'$ factors uniquely through a linear map $V \otimes V' \to V \otimes V'$, which we call $(\rho \otimes \rho')(g)$. Each $(\rho \otimes \rho')(g)$ is invertible with inverse $(\rho \otimes \rho')(g^{-1})$ (verified once we establish the homomorphism property), so it lies in $\operatorname{GL}(V \otimes V')$. For the homomorphism property, fix $g_1, g_2 \in G$. On a pure tensor $v \otimes w$, \begin{align*} (\rho \otimes \rho')(g_1)\bigl[(\rho \otimes \rho')(g_2)(v \otimes w)\bigr] &= (\rho \otimes \rho')(g_1)\bigl[\rho(g_2)v \otimes \rho'(g_2)w\bigr] \\ &= \rho(g_1)\rho(g_2)v \otimes \rho'(g_1)\rho'(g_2)w \\ &= \rho(g_1 g_2)v \otimes \rho'(g_1 g_2)w \\ &= (\rho \otimes \rho')(g_1 g_2)(v \otimes w). \end{align*} The first equality applies the definition of $(\rho \otimes \rho')(g_2)$. The second applies the definition of $(\rho \otimes \rho')(g_1)$ to the pure tensor $\rho(g_2)v \otimes \rho'(g_2)w$. The third uses that $\rho$ and $\rho'$ are group homomorphisms. The fourth applies the definition of $(\rho \otimes \rho')(g_1 g_2)$. The two linear endomorphisms $(\rho \otimes \rho')(g_1)(\rho \otimes \rho')(g_2)$ and $(\rho \otimes \rho')(g_1 g_2)$ of $V \otimes V'$ agree on every pure tensor. Since pure tensors span $V \otimes V'$, the two endomorphisms agree everywhere by linearity. Also $(\rho \otimes \rho')(1_G)(v \otimes w) = v \otimes w$ since $\rho(1_G) = I_V$ and $\rho'(1_G) = I_{V'}$, so $(\rho \otimes \rho')(1_G) = I_{V \otimes V'}$. Hence $\rho \otimes \rho'$ is a representation of $G$ on $V \otimes V'$. [guided] Two questions: why is $(\rho \otimes \rho')(g)$ a well-defined linear map on $V \otimes V'$, and why is the assignment $g \mapsto (\rho \otimes \rho')(g)$ a homomorphism? For well-definedness, the map \begin{align*} \beta_g: V \times V' &\to V \otimes V', \\ (v, w) &\mapsto \rho(g)v \otimes \rho'(g)w \end{align*} is bilinear: it is linear in $v$ because $\rho(g)$ is linear and $\otimes$ is linear in its first argument; it is linear in $w$ for the symmetric reason. By the universal property of the tensor product, $\beta_g$ extends to a unique linear map $V \otimes V' \to V \otimes V'$, which we call $(\rho \otimes \rho')(g)$. The formula in the statement is exactly this extension applied to a general element, written as a finite linear combination of pure tensors. For the homomorphism property, the computation is on pure tensors and uses only that $\rho$ and $\rho'$ are individually homomorphisms; the tensor structure is preserved automatically. The four-line chain reads: apply $g_2$ first (entries become $\rho(g_2)v$ and $\rho'(g_2)w$), then $g_1$ on top (entries become $\rho(g_1)\rho(g_2)v$ and $\rho'(g_1)\rho'(g_2)w$), use the homomorphism property in each factor separately (entries become $\rho(g_1 g_2)v$ and $\rho'(g_1 g_2)w$), and recognise the result as $(\rho \otimes \rho')(g_1 g_2)$ applied to the original pure tensor. The conclusion on pure tensors extends to all of $V \otimes V'$ by linearity, since pure tensors $v \otimes w$ span $V \otimes V'$. (More than spanning, $\{v_i \otimes w_j\}$ is a basis when $\{v_i\}$ and $\{w_j\}$ are bases of $V$ and $V'$, which we will use in Step 2.) [/guided] [/step] [step:Simultaneously diagonalise $\rho(g)$ and $\rho'(g)$ to produce an eigenbasis of $V \otimes V'$] Fix $g \in G$. Since $G$ is finite, the operators $\rho(g) \in \operatorname{GL}(V)$ and $\rho'(g) \in \operatorname{GL}(V')$ both have finite order. As in the standard argument (the minimal polynomial divides $X^m - 1$ for some $m$, which has distinct complex roots), each is diagonalisable over $\mathbb{C}$. Choose a basis $v_1, \ldots, v_m$ of $V$ with $\rho(g)v_i = \lambda_i v_i$, and a basis $w_1, \ldots, w_n$ of $V'$ with $\rho'(g)w_j = \mu_j w_j$. The vectors $\{v_i \otimes w_j : 1 \leq i \leq m,\, 1 \leq j \leq n\}$ form a basis of $V \otimes V'$ of dimension $mn$. For each $(i,j)$, \begin{align*} (\rho \otimes \rho')(g)(v_i \otimes w_j) = (\rho(g)v_i) \otimes (\rho'(g)w_j) = (\lambda_i v_i) \otimes (\mu_j w_j) = \lambda_i \mu_j\, (v_i \otimes w_j). \end{align*} The third equality uses bilinearity of $\otimes$: scalars factor out of either argument. So $v_i \otimes w_j$ is an eigenvector of $(\rho \otimes \rho')(g)$ with eigenvalue $\lambda_i \mu_j$, and $\{v_i \otimes w_j\}$ diagonalises $(\rho \otimes \rho')(g)$. [/step] [step:Sum the eigenvalues to obtain the product character formula] By Step 2, the trace of $(\rho \otimes \rho')(g)$ is the sum of its eigenvalues, indexed by the basis $\{v_i \otimes w_j\}$: \begin{align*} \chi_{\rho \otimes \rho'}(g) = \operatorname{tr}\bigl((\rho \otimes \rho')(g)\bigr) = \sum_{i=1}^m \sum_{j=1}^n \lambda_i \mu_j = \biggl(\sum_{i=1}^m \lambda_i\biggr)\biggl(\sum_{j=1}^n \mu_j\biggr). \end{align*} The double sum factors because $\lambda_i \mu_j$ is a product. Identifying the factors with traces: \begin{align*} \sum_{i=1}^m \lambda_i = \operatorname{tr}(\rho(g)) = \chi_\rho(g), \qquad \sum_{j=1}^n \mu_j = \operatorname{tr}(\rho'(g)) = \chi_{\rho'}(g). \end{align*} Therefore \begin{align*} \chi_{\rho \otimes \rho'}(g) = \chi_\rho(g)\, \chi_{\rho'}(g) \end{align*} for every $g \in G$. [guided] The character formula is a direct consequence of the eigenvalue structure. Two finite-order operators on finite-dimensional complex vector spaces, acting independently on the two tensor factors, produce a tensor operator whose eigenvalues are exactly the products $\lambda_i \mu_j$ over all pairs. The trace of any diagonalisable operator is the sum of its eigenvalues. Here: \begin{align*} \operatorname{tr}\bigl((\rho \otimes \rho')(g)\bigr) = \sum_{i,j} \lambda_i \mu_j. \end{align*} The double sum factors as a product of single sums because $\lambda_i \mu_j$ has separated dependence on $i$ and $j$: \begin{align*} \sum_{i,j} \lambda_i \mu_j = \sum_i \lambda_i \sum_j \mu_j. \end{align*} This is the same factorisation that appears in $\sum_{i,j} a_i b_j = (\sum_i a_i)(\sum_j b_j)$ for any product-of-sums distribution. The final step identifies the two factors with the original characters: $\sum_i \lambda_i = \operatorname{tr}(\rho(g)) = \chi_\rho(g)$ and similarly for $\rho'$. So \begin{align*} \chi_{\rho \otimes \rho'}(g) = \chi_\rho(g) \cdot \chi_{\rho'}(g). \end{align*} The character of the tensor product representation is the **pointwise product** of the characters. This is one of the fundamental operations in the character ring $R(G)$: the character ring is closed under pointwise multiplication, with $\chi_\rho \chi_{\rho'}$ being the character of $\rho \otimes \rho'$. [/guided] [/step]