Pauli group

-- Pauli operators
def Z := ∑ j, exp(2 i π j /d) |j⟩⟨j|

def X := ∑ k, |j+1⟩⟨j|

example : Z^d = X^d = 1 := sorry

/--
The Pauli group for one system
-/
def P d := {exp(i π k /d) Z^a X^b | a,b ∈ ℤ_d, k ∈ ℤ_2d}

/--
The Pauli group for multiple systems.
-/
def P d n := {M₁ ⊗ ... ⊗ Mₙ : Mⱼ ∈ P d}

“The set of all these tensor products, up to -1 or ±i, forms a group 𝒢 under multiplication: The Pauli group. For n qubits the Pauli group is 𝒢ₙ := {±1,±i} ⊗ {I,X,Y,Z}^{⊗ⁿ}.”

-- Why is this a group?

example : X^b Z^a = exp(-2 π i a b / d) Z^a X^b := sorry

example : span (P d n) = M(dⁿ;ℂ) := sorry

example : Tr Zᵃ Xᵇ Zᵃ' Xᵇ' ∝ δₐₐ' δbb'

/--
The conjugate of a Pauli is a Pauli
-/
lemma conjugate_of_Pauli : ... := sorry

• The Pauli group plays a major role in the Stabilizer formalism.