WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Pauli matrices

Revision #1462 → #3165 · back to history

modifiedTransposition (permutation) operatorda56eeeed397
FieldFrom #1462To #3165
mathlib.moduleMathlib.Logic.Equiv.DefsMathlib.Logic.Equiv.Basic
noteGeneric transposition Equiv.swap exists, but the spin-exchange operator is not.Generic transposition Equiv.swap exists in Mathlib.Logic.Equiv.Basic, but the spin-exchange operator is not.
addedPauli matrices are traceless, Hermitian, involutory, and unitary56836a09f4dd
addedPauli algebra isomorphic to quaternions4b7103e6d8db
addedCompleteness relation for the Pauli 4-vector3d5e6a24511c