Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,867 to 1,872 of 2,569 results.
PauliMatrix.pauliCo_contr_pauliContr
Mathematical statement
The statement that σᵥᵃᵇ σᵛᵃ'ᵇ' = 2 εᵃᵃ' εᵇᵇ'.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint_linearly_independent
Mathematical statement
The Pauli matrices are linearly independent.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint_span
Mathematical statement
The Pauli matrices span all self-adjoint matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint'_linearly_independent
Mathematical statement
The Pauli matrices where σi are negated are linearly independent.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint'_span
Mathematical statement
The Pauli matrices where σi are negated span all Self-adjoint matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.selfAdjoint_ext
Mathematical statement
Two 2×2 self-adjoint matrices are equal if the real traces of each matrix multiplied by each of the Pauli-matrices are equal.
Source project: Physlib
Person-level attribution pending.