PhysLean.Relativity.PauliMatrices.Matrix

Pauli matrices #

@[reducible, inline]

The zeroth Pauli-matrix as a 2 x 2 complex matrix. That is the matrix !![1, 0; 0, 1], which in Lean is more conveniently written 1.

Equations

PauliMatrix.σ0 = 1

Instances For

source

theorem PauliMatrix.σ0_eq :

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

source

def PauliMatrix.σ1 :

Matrix (Fin 2) (Fin 2) ℂ

The first Pauli-matrix as a 2 x 2 complex matrix. That is, the matrix !![0, 1; 1, 0].

Equations

PauliMatrix.σ1 = !![0, 1; 1, 0]

Instances For

source

def PauliMatrix.σ2 :

Matrix (Fin 2) (Fin 2) ℂ

The second Pauli-matrix as a 2 x 2 complex matrix. That is, the matrix !![0, -I; I, 0].

Equations

PauliMatrix.σ2 = !![0, -Complex.I; Complex.I, 0]

Instances For

source

def PauliMatrix.σ3 :

Matrix (Fin 2) (Fin 2) ℂ

The third Pauli-matrix as a 2 x 2 complex matrix. That is, the matrix !![1, 0; 0, -1].

Equations

PauliMatrix.σ3 = !![1, 0; 0, -1]

Instances For

source

theorem PauliMatrix.σ0_selfAdjoint :

σ0.conjTranspose = σ0

The conjugate transpose of σ0 is equal to σ0.

source

@[simp]

theorem PauliMatrix.σ1_selfAdjoint :

σ1.conjTranspose = σ1

The conjugate transpose of σ1 is equal to σ1.

source

@[simp]

theorem PauliMatrix.σ2_selfAdjoint :

σ2.conjTranspose = σ2

The conjugate transpose of σ2 is equal to σ2.

source

@[simp]

theorem PauliMatrix.σ3_selfAdjoint :

σ3.conjTranspose = σ3

The conjugate transpose of σ3 is equal to σ3.

Products #

These lemmas try to put the terms in numerical order. We skip σ0 since it's just 1 anyway.

source

@[simp]

theorem PauliMatrix.σ1_mul_σ1 :

σ1 * σ1 = 1

source

@[simp]

theorem PauliMatrix.σ2_mul_σ2 :

σ2 * σ2 = 1

source

@[simp]

theorem PauliMatrix.σ3_mul_σ3 :

σ3 * σ3 = 1

source

@[simp]

theorem PauliMatrix.σ2_mul_σ1 :

σ2 * σ1 = -(σ1 * σ2)

source

@[simp]

theorem PauliMatrix.σ3_mul_σ1 :

σ3 * σ1 = -(σ1 * σ3)

source

@[simp]

theorem PauliMatrix.σ3_mul_σ2 :

σ3 * σ2 = -(σ2 * σ3)

Traces #

source

@[simp]

theorem PauliMatrix.trace_σ1 :

σ1.trace = 0

source

@[simp]

theorem PauliMatrix.trace_σ2 :

σ2.trace = 0

source

@[simp]

theorem PauliMatrix.trace_σ3 :

σ3.trace = 0

source

theorem PauliMatrix.σ0_σ0_trace :

(σ0 * σ0).trace = 2

The trace of σ0 multiplied by σ0 is equal to 2.

source

theorem PauliMatrix.σ0_σ1_trace :

(σ0 * σ1).trace = 0

The trace of σ0 multiplied by σ1 is equal to 0.

source

theorem PauliMatrix.σ0_σ2_trace :

(σ0 * σ2).trace = 0

The trace of σ0 multiplied by σ2 is equal to 0.

source

theorem PauliMatrix.σ0_σ3_trace :

(σ0 * σ3).trace = 0

The trace of σ0 multiplied by σ3 is equal to 0.

source

theorem PauliMatrix.σ1_σ0_trace :

(σ1 * σ0).trace = 0

The trace of σ1 multiplied by σ0 is equal to 0.

source

theorem PauliMatrix.σ1_σ1_trace :

(σ1 * σ1).trace = 2

The trace of σ1 multiplied by σ1 is equal to 2.

source

@[simp]

theorem PauliMatrix.σ1_σ2_trace :

(σ1 * σ2).trace = 0

The trace of σ1 multiplied by σ2 is equal to 0.

source

@[simp]

theorem PauliMatrix.σ1_σ3_trace :

(σ1 * σ3).trace = 0

The trace of σ1 multiplied by σ3 is equal to 0.

source

theorem PauliMatrix.σ2_σ0_trace :

(σ2 * σ0).trace = 0

The trace of σ2 multiplied by σ0 is equal to 0.

source

theorem PauliMatrix.σ2_σ1_trace :

(σ2 * σ1).trace = 0

The trace of σ2 multiplied by σ1 is equal to 0.

source

theorem PauliMatrix.σ2_σ2_trace :

(σ2 * σ2).trace = 2

The trace of σ2 multiplied by σ2 is equal to 2.

source

@[simp]

theorem PauliMatrix.σ2_σ3_trace :

(σ2 * σ3).trace = 0

The trace of σ2 multiplied by σ3 is equal to 0.

source

theorem PauliMatrix.σ3_σ0_trace :

(σ3 * σ0).trace = 0

The trace of σ3 multiplied by σ0 is equal to 0.

source

theorem PauliMatrix.σ3_σ1_trace :

(σ3 * σ1).trace = 0

The trace of σ3 multiplied by σ1 is equal to 0.

source

theorem PauliMatrix.σ3_σ2_trace :

(σ3 * σ2).trace = 0

The trace of σ3 multiplied by σ2 is equal to 0.

source

theorem PauliMatrix.σ3_σ3_trace :

(σ3 * σ3).trace = 2

The trace of σ3 multiplied by σ3 is equal to 2.