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 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.leftMetricVal_expand_tmul
Plain-language statement
Expansion of leftMetricVal into the left basis.
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.rightMetricVal_expand_tmul
Plain-language statement
Expansion of rightMetricVal into the left basis.
Source project: Physlib
Person-level attribution pending.