Documentation

LCS.Pauli

def I2 :

Matrix (Fin 2) (Fin 2) ℂ

Equations

I2 = !![1, 0; 0, 1]

Instances For

def X :

Matrix (Fin 2) (Fin 2) ℂ

Equations

X = !![0, 1; 1, 0]

Instances For

def Y :

Matrix (Fin 2) (Fin 2) ℂ

Equations

Y = !![0, -Complex.I; Complex.I, 0]

Instances For

def Z :

Matrix (Fin 2) (Fin 2) ℂ

Equations

Z = !![1, 0; 0, -1]

Instances For

theorem I2_eq_one :

I2 = 1

theorem I2_comm_left (P : Matrix (Fin 2) (Fin 2) ℂ) :

theorem I2_comm_right (P : Matrix (Fin 2) (Fin 2) ℂ) :

theorem I2_sq :

theorem X_sq :

X * X = 1

theorem Y_sq :

Y * Y = 1

theorem Z_sq :

Z * Z = 1

theorem I2_selfAdjoint :

theorem X_selfAdjoint :

theorem Y_selfAdjoint :

theorem Z_selfAdjoint :

theorem XY_mul :

X * Y = Complex.I • Z

theorem YX_mul :

Y * X = -Complex.I • Z

theorem XZ_mul :

X * Z = -Complex.I • Y

theorem ZX_mul :

Z * X = Complex.I • Y

theorem YZ_mul :

Y * Z = Complex.I • X

theorem ZY_mul :

Z * Y = -Complex.I • X

theorem XY_anticomm :

X * Y = -(Y * X)

theorem XZ_anticomm :

X * Z = -(Z * X)

theorem YZ_anticomm :

Y * Z = -(Z * Y)

theorem I2_observable :

IsObservable I2

theorem X_observable :

theorem Y_observable :

theorem Z_observable :

theorem kronecker_comm_of_comm {A B C D : Matrix (Fin 2) (Fin 2) ℂ} (hAC : Commute A C) (hBD : Commute B D) :

Commute (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) C D)

theorem kronecker_comm_of_anticomm {A B C D : Matrix (Fin 2) (Fin 2) ℂ} (hAC : A * C = -(C * A)) (hBD : B * D = -(D * B)) :

Commute (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) C D)

theorem kronecker_observable {A B : Matrix (Fin 2) (Fin 2) ℂ} (hA : IsObservable A) (hB : IsObservable B) :

IsObservable (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B)