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 591 research declarations. Search 10,000 more complete Mathlib declarations.
591 results
Clear filtersPauliMatrix.pauliBasis'_repr_inl_0
Plain-language statement
The component of a self-adjoint matrix in the direction σ0 under the basis formed by the covariant Pauli matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliBasis'_repr_inr_0
Plain-language statement
The component of a self-adjoint matrix in the direction -σ1 under the basis formed by the covariant Pauli matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliBasis'_repr_inr_1
Plain-language statement
The component of a self-adjoint matrix in the direction -σ2 under the basis formed by the covariant Pauli matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.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.pauliCo_contr_pauliContr
Plain-language statement
The statement that σᵥᵃᵇ σᵛᵃ'ᵇ' = 2 εᵃᵃ' εᵇᵇ'.
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.