9. Clifford group structure
Let us define the semidirect product of \SL(2,ℤ_d) and ℤ_d^2.
The semidirect product \SL(2,ℤ_d) \ltimes ℤ_d^2 consists of pairs (F, \bchi) \in \SL(2,ℤ_d) \times ℤ_d^2 with composition given by
(F_1, \bchi_1) \cdot (F_2, \bchi_2) = (F_1 F_2,\, \bchi_1 + F_1 \bchi_2).
The main result of our formalization is the following theorem that describes the structure of the Clifford group in dimension d that is an odd prime.
It corresponds to Theorem 1 in Appleby (2005).
Let d be an odd prime.
Let \mathrm{I}(d) = \{ e^{i\theta} I : \theta \in \mathbb{R} \} be the subgroup of \Cliff(d) from Definition 6.1 consisting of all scalar multiples of the identity.
There exists a unique group isomorphism
f \colon \SL(2,ℤ_d) \ltimes ℤ_d^2 \to \Cliff(d)/\mathrm{I}(d)
such that for each U in the coset f(F, \bchi) and all \p \in ℤ^2,
U D_{\p} U^\dagger = \omega^{\langle \bchi, F\p \rangle} D_{F\p}
where \omega is the d-th root of unity from Definition 2.2, D_\p is the displacement operator from Definition 5.1, and \braket{\cdot,\cdot} is the symplectic inner product from Definition 3.1.
This theorem allows us to compute the size of the Clifford group, see Lemma 5 in Appleby (2005).