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 18 research declarations. Search 10,000 more complete Mathlib declarations.
18 results
Clear filtersFermion.leftLeftToMatrix_ρ
Plain-language statement
The group action of SL(2,ℂ) on leftHanded ⊗ leftHanded is equivalent to M.1 * leftLeftToMatrix v * (M.1)ᵀ.
Source project: Physlib
Person-level attribution pending.
Fermion.leftRightToMatrix_symm_expand_tmul
Plain-language statement
Expanding leftRightToMatrix in terms of the standard basis.
Source project: Physlib
Person-level attribution pending.
Fermion.rightDualRightToMatrix_symm_expand_tmul
Plain-language statement
Expanding rightDualRightToMatrix in terms of the standard basis.
Source project: Physlib
Person-level attribution pending.
Fermion.rightDualRightToMatrix_ρ
Plain-language statement
The group action of SL(2,ℂ) on rightHanded ⊗ dualRightHanded is equivalent to (M.1.map star) * rightDualRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ.
Source project: Physlib
Person-level attribution pending.
Fermion.rightRightToMatrix_symm_expand_tmul
Plain-language statement
Expanding rightRightToMatrix in terms of the standard basis.
Source project: Physlib
Person-level attribution pending.
Fermion.rightRightToMatrix_ρ
Plain-language statement
The group action of SL(2,ℂ) on rightHanded ⊗ rightHanded is equivalent to (M.1.map star) * rightRightToMatrix v * ((M.1.map star))ᵀ.
Source project: Physlib
Person-level attribution pending.