Is the Pauli group for $n$-qubits a basis for $\mathbb{C}^{2^n\times 2^n}$?

The Pauli group for $n$-qubits is defined as $G_n=\{I,X,Y,Z \}^{\otimes n}$, that is as the group containing all the possible tensor products between $n$ Pauli matrices. It is clear that the Pauli matrices form a basis for the $2\times 2$ complex matrix vector spaces, that is $\mathbb{C}^{2\times 2}$. Apart from it, from the definition of the tensor product, it is known that the $n$-qubit Pauli group will form a basis for the tensor product space $(\mathbb{C}^{2\times 2})^{\otimes n}$.

I am wondering if the Pauli group in $n$-qubits forms a basis for the complex vector space where the elements of this tensor product space act, that is $\mathbb{C}^{2^n\times 2^n}$. Summarizing, the question would be, is $(\mathbb{C}^{2\times 2})^{\otimes n}=\mathbb{C}^{2^n\times 2^n}$ true?

I have been trying to prove it using arguments about the dimensions of both spaces, but I have not been able to get anything yet.

Yes, the set of tensor products of all possible $n$ Pauli operators (including $I$) forms an orthogonal basis for the vector space of $2^n \times 2^n$ complex matrices. So see this first we notice that the space has a dimension of $4^n$ and we also have $4^n$ vectors ( the vectors are operators in this case). So we only need to show that they are linearly independent.
We can actually show something stronger. It can be easily seen that the members of the Pauli group are orthogonal under the Hilbert-Schmidt inner product. The H-S inner product of two matrices is defined as $Tr(AB^\dagger)$. We can easily verify from the definition that the Pauli group is a mutually orthogonal set under this inner product. We simply have to use the elementary property $Tr(C \otimes D) = Tr(C)Tr(D)$.
• @biryaniTo prove that the new set you obtained is linearly independent, wouldn't you need to prove that $Tr(AB)=0$ for every $A$ and $B$ of the new set? In that case, I haven't understood how the trace propriety with respect to the tensor product comes into play. When you compute $Tr(A_1 \otimes ... \otimes A_n) = Tr(A_1)...Tr(A_n)$ you are computing the trace of a new element of the set but not the trace of the product of the elements of that set $Tr(AB)$. In the latter case, it's not allowed to write $Tr(AB)=Tr(A)Tr(B)$ and then expand the two traces as you proposed, so I missed a step. – Enrico Sep 26 '20 at 10:08