PhysLean.Relativity.Lorentz.PauliMatrices.Matrix

Pauli matrices #

source

def PauliMatrix.σ0 :

Matrix (Fin 2) (Fin 2) ℂ

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

Equations

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

Instances For

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

@[simp]

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.

Traces #

source

@[simp]

theorem PauliMatrix.σ0_σ0_trace :

(σ0 * σ0).trace = 2

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

source

@[simp]

theorem PauliMatrix.σ0_σ1_trace :

(σ0 * σ1).trace = 0

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

source

@[simp]

theorem PauliMatrix.σ0_σ2_trace :

(σ0 * σ2).trace = 0

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

source

@[simp]

theorem PauliMatrix.σ0_σ3_trace :

(σ0 * σ3).trace = 0

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

source

@[simp]

theorem PauliMatrix.σ1_σ0_trace :

(σ1 * σ0).trace = 0

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

source

@[simp]

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

@[simp]

theorem PauliMatrix.σ2_σ0_trace :

(σ2 * σ0).trace = 0

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

source

@[simp]

theorem PauliMatrix.σ2_σ1_trace :

(σ2 * σ1).trace = 0

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

source

@[simp]

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

@[simp]

theorem PauliMatrix.σ3_σ0_trace :

(σ3 * σ0).trace = 0

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

source

@[simp]

theorem PauliMatrix.σ3_σ1_trace :

(σ3 * σ1).trace = 0

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

source

@[simp]

theorem PauliMatrix.σ3_σ2_trace :

(σ3 * σ2).trace = 0

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

source

@[simp]

theorem PauliMatrix.σ3_σ3_trace :

(σ3 * σ3).trace = 2

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