PhysLean Documentation

PhysLean.Relativity.Lorentz.PauliMatrices.Relations

Contractiong of indices of Pauli matrix. #

The main result of this file is pauliMatrix_contract_pauliMatrix which states that η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}.

The current way this result is proved is by using tensor tree manipulations. There is likely a more direct path to this result.