Solution (source code)

= Solution

The four displayed matrices fail <closure>: for example $\sigma_x\sigma_y=i\sigma_z$ is not one of them. Thus they do not form a <group> by themselves.

Let $\sigma_0=I$ and $\mu_4=\{1,-1,i,-i\}$. The enlarged set is the single-qubit <Pauli group>
$$
\boxed{\mathcal P_1=\{\eta\sigma_a:\eta\in\mu_4,\ a\in\{0,x,y,z\}\}.}
$$
There are 16 distinct matrices: $I,\sigma_x,\sigma_y,\sigma_z$ are linearly independent, so two different ones cannot be scalar multiples, and the four phases are distinct for each nonzero matrix.

The <Pauli matrices> satisfy
$$
\sigma_a\sigma_b=\delta_{ab}I+i\epsilon_{abc}\sigma_c\quad(a,b\in\{x,y,z\}),\qquad\sigma_a^2=I.
$$
Here $\delta$ is the <Kronecker delta> and $\epsilon$ the <Levi-Civita symbol>. Thus any product of two Pauli matrices is another Pauli matrix or the identity times a phase in $\mu_4$. Multiplying by the two original phases preserves membership in $\mu_4$, proving <closure> of all 16 matrices.

<Associativity> is inherited from <matrix multiplication>, the identity is $I$, and
$$
(\eta\sigma_a)^{-1}=\eta^{-1}\sigma_a\in\mathcal P_1.
$$
This proves every group axiom. The resulting group is non-Abelian, since reversing $\sigma_x\sigma_y$ changes its sign.