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 13 research declarations. Search 10,000 more complete Mathlib declarations.
13 results
Clear filtersPauliMatrix.pauliBasis'_repr_inr_2
Plain-language statement
The component of a self-adjoint matrix in the direction -σ3 under the basis formed by the covariant Pauli matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint_linearly_independent
Plain-language statement
The Pauli matrices are linearly independent.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint_span
Plain-language statement
The Pauli matrices span all self-adjoint matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint'_linearly_independent
Plain-language statement
The Pauli matrices where σi are negated are linearly independent.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint'_span
Plain-language statement
The Pauli matrices where σi are negated span all Self-adjoint matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.selfAdjoint_ext
Plain-language 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.