Two

📁 Source: PhysLean/Relativity/Tensors/ComplexTensor/Weyl/Two.lean

Statistics

Metric	Count
Definitions `altLeftAltRightToMatrix`, `altLeftLeftToMatrix`, `altLeftaltLeftToMatrix`, `altRightAltRightToMatrix`, `altRightRightToMatrix`, `leftAltLeftToMatrix`, `leftLeftToMatrix`, `leftRightToMatrix`, `rightAltRightToMatrix`, `rightRightToMatrix`	10
Theorems `altLeftAltRightToMatrix_symm_expand_tmul`, `altLeftAltRightToMatrix_ρ`, `altLeftAltRightToMatrix_ρ_symm`, `altLeftAltRightToMatrix_ρ_symm_selfAdjoint`, `altLeftLeftToMatrix_symm_expand_tmul`, `altLeftLeftToMatrix_ρ`, `altLeftLeftToMatrix_ρ_symm`, `altLeftaltLeftToMatrix_symm_expand_tmul`, `altLeftaltLeftToMatrix_ρ`, `altLeftaltLeftToMatrix_ρ_symm`, `altRightAltRightToMatrix_symm_expand_tmul`, `altRightAltRightToMatrix_ρ`, `altRightAltRightToMatrix_ρ_symm`, `altRightRightToMatrix_symm_expand_tmul`, `altRightRightToMatrix_ρ`, `altRightRightToMatrix_ρ_symm`, `leftAltLeftToMatrix_symm_expand_tmul`, `leftAltLeftToMatrix_ρ`, `leftAltLeftToMatrix_ρ_symm`, `leftLeftToMatrix_symm_expand_tmul`, `leftLeftToMatrix_ρ`, `leftLeftToMatrix_ρ_symm`, `leftRightToMatrix_symm_expand_tmul`, `leftRightToMatrix_ρ`, `leftRightToMatrix_ρ_symm`, `leftRightToMatrix_ρ_symm_selfAdjoint`, `rightAltRightToMatrix_symm_expand_tmul`, `rightAltRightToMatrix_ρ`, `rightAltRightToMatrix_ρ_symm`, `rightRightToMatrix_symm_expand_tmul`, `rightRightToMatrix_ρ`, `rightRightToMatrix_ρ_symm`	32
Total	42

Fermion

Definitions

Name	Category	Theorems
`altLeftAltRightToMatrix` 📖	CompOp	4 math math: `altLeftAltRightToMatrix_ρ`, `altLeftAltRightToMatrix_ρ_symm`, `altLeftAltRightToMatrix_ρ_symm_selfAdjoint`, `altLeftAltRightToMatrix_symm_expand_tmul`
`altLeftLeftToMatrix` 📖	CompOp	3 math math: `altLeftLeftToMatrix_ρ`, `altLeftLeftToMatrix_ρ_symm`, `altLeftLeftToMatrix_symm_expand_tmul`
`altLeftaltLeftToMatrix` 📖	CompOp	3 math math: `altLeftaltLeftToMatrix_ρ`, `altLeftaltLeftToMatrix_symm_expand_tmul`, `altLeftaltLeftToMatrix_ρ_symm`
`altRightAltRightToMatrix` 📖	CompOp	3 math math: `altRightAltRightToMatrix_symm_expand_tmul`, `altRightAltRightToMatrix_ρ`, `altRightAltRightToMatrix_ρ_symm`
`altRightRightToMatrix` 📖	CompOp	3 math math: `altRightRightToMatrix_ρ`, `altRightRightToMatrix_ρ_symm`, `altRightRightToMatrix_symm_expand_tmul`
`leftAltLeftToMatrix` 📖	CompOp	3 math math: `leftAltLeftToMatrix_symm_expand_tmul`, `leftAltLeftToMatrix_ρ`, `leftAltLeftToMatrix_ρ_symm`
`leftLeftToMatrix` 📖	CompOp	3 math math: `leftLeftToMatrix_symm_expand_tmul`, `leftLeftToMatrix_ρ`, `leftLeftToMatrix_ρ_symm`
`leftRightToMatrix` 📖	CompOp	9 math math: `leftRightToMatrix_ρ_symm`, `PauliMatrix.leftRightToMatrix_σSA_inl_0_expand`, `leftRightToMatrix_ρ_symm_selfAdjoint`, `PauliMatrix.leftRightToMatrix_σSA_inr_1_expand`, `PauliMatrix.asTensor_expand_complexContrBasis`, `leftRightToMatrix_symm_expand_tmul`, `PauliMatrix.leftRightToMatrix_σSA_inr_0_expand`, `leftRightToMatrix_ρ`, `PauliMatrix.leftRightToMatrix_σSA_inr_2_expand`
`rightAltRightToMatrix` 📖	CompOp	3 math math: `rightAltRightToMatrix_symm_expand_tmul`, `rightAltRightToMatrix_ρ`, `rightAltRightToMatrix_ρ_symm`
`rightRightToMatrix` 📖	CompOp	3 math math: `rightRightToMatrix_ρ`, `rightRightToMatrix_ρ_symm`, `rightRightToMatrix_symm_expand_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`altLeftAltRightToMatrix_symm_expand_tmul` 📖	mathematical	—	`altLeftHanded` `altRightHanded` `altLeftAltRightToMatrix` `altLeftBasis` `altRightBasis`	—	—
`altLeftAltRightToMatrix_ρ` 📖	mathematical	—	`altLeftHanded` `altRightHanded` `altLeftAltRightToMatrix`	—	`altLeftAltRightToMatrix.eq_1` `altLeftBasis_ρ_apply` `altRightBasis_ρ_apply`
`altLeftAltRightToMatrix_ρ_symm` 📖	mathematical	—	`altLeftHanded` `altRightHanded` `altLeftAltRightToMatrix`	—	`altLeftAltRightToMatrix_ρ`
`altLeftAltRightToMatrix_ρ_symm_selfAdjoint` 📖	mathematical	—	`altLeftHanded` `altRightHanded` `altLeftAltRightToMatrix` `Lorentz.SL2C.toSelfAdjointMap`	—	`altLeftAltRightToMatrix_ρ_symm` `Lorentz.SL2C.inverse_coe`
`altLeftLeftToMatrix_symm_expand_tmul` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftLeftToMatrix` `altLeftBasis` `leftBasis`	—	—
`altLeftLeftToMatrix_ρ` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftLeftToMatrix`	—	`altLeftLeftToMatrix.eq_1` `altLeftBasis_ρ_apply` `leftBasis_ρ_apply`
`altLeftLeftToMatrix_ρ_symm` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftLeftToMatrix`	—	`altLeftLeftToMatrix_ρ`
`altLeftaltLeftToMatrix_symm_expand_tmul` 📖	mathematical	—	`altLeftHanded` `altLeftaltLeftToMatrix` `altLeftBasis`	—	—
`altLeftaltLeftToMatrix_ρ` 📖	mathematical	—	`altLeftHanded` `altLeftaltLeftToMatrix`	—	`altLeftaltLeftToMatrix.eq_1` `altLeftBasis_ρ_apply`
`altLeftaltLeftToMatrix_ρ_symm` 📖	mathematical	—	`altLeftHanded` `altLeftaltLeftToMatrix`	—	`altLeftaltLeftToMatrix_ρ`
`altRightAltRightToMatrix_symm_expand_tmul` 📖	mathematical	—	`altRightHanded` `altRightAltRightToMatrix` `altRightBasis`	—	—
`altRightAltRightToMatrix_ρ` 📖	mathematical	—	`altRightHanded` `altRightAltRightToMatrix`	—	`altRightAltRightToMatrix.eq_1` `altRightBasis_ρ_apply`
`altRightAltRightToMatrix_ρ_symm` 📖	mathematical	—	`altRightHanded` `altRightAltRightToMatrix`	—	`altRightAltRightToMatrix_ρ`
`altRightRightToMatrix_symm_expand_tmul` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightRightToMatrix` `altRightBasis` `rightBasis`	—	—
`altRightRightToMatrix_ρ` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightRightToMatrix`	—	`altRightRightToMatrix.eq_1` `altRightBasis_ρ_apply` `rightBasis_ρ_apply`
`altRightRightToMatrix_ρ_symm` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightRightToMatrix`	—	`altRightRightToMatrix_ρ`
`leftAltLeftToMatrix_symm_expand_tmul` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltLeftToMatrix` `leftBasis` `altLeftBasis`	—	—
`leftAltLeftToMatrix_ρ` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltLeftToMatrix`	—	`leftAltLeftToMatrix.eq_1` `leftBasis_ρ_apply` `altLeftBasis_ρ_apply`
`leftAltLeftToMatrix_ρ_symm` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltLeftToMatrix`	—	`leftAltLeftToMatrix_ρ`
`leftLeftToMatrix_symm_expand_tmul` 📖	mathematical	—	`leftHanded` `leftLeftToMatrix` `leftBasis`	—	—
`leftLeftToMatrix_ρ` 📖	mathematical	—	`leftHanded` `leftLeftToMatrix`	—	`leftLeftToMatrix.eq_1` `leftBasis_ρ_apply`
`leftLeftToMatrix_ρ_symm` 📖	mathematical	—	`leftHanded` `leftLeftToMatrix`	—	`leftLeftToMatrix_ρ`
`leftRightToMatrix_symm_expand_tmul` 📖	mathematical	—	`leftHanded` `rightHanded` `leftRightToMatrix` `leftBasis` `rightBasis`	—	—
`leftRightToMatrix_ρ` 📖	mathematical	—	`leftHanded` `rightHanded` `leftRightToMatrix`	—	`leftRightToMatrix.eq_1` `leftBasis_ρ_apply` `rightBasis_ρ_apply`
`leftRightToMatrix_ρ_symm` 📖	mathematical	—	`leftHanded` `rightHanded` `leftRightToMatrix`	—	`leftRightToMatrix_ρ`
`leftRightToMatrix_ρ_symm_selfAdjoint` 📖	mathematical	—	`leftHanded` `rightHanded` `leftRightToMatrix` `Lorentz.SL2C.toSelfAdjointMap`	—	`leftRightToMatrix_ρ_symm`
`rightAltRightToMatrix_symm_expand_tmul` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltRightToMatrix` `rightBasis` `altRightBasis`	—	—
`rightAltRightToMatrix_ρ` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltRightToMatrix`	—	`rightAltRightToMatrix.eq_1` `rightBasis_ρ_apply` `altRightBasis_ρ_apply`
`rightAltRightToMatrix_ρ_symm` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltRightToMatrix`	—	`rightAltRightToMatrix_ρ`
`rightRightToMatrix_symm_expand_tmul` 📖	mathematical	—	`rightHanded` `rightRightToMatrix` `rightBasis`	—	—
`rightRightToMatrix_ρ` 📖	mathematical	—	`rightHanded` `rightRightToMatrix`	—	`rightRightToMatrix.eq_1` `rightBasis_ρ_apply`
`rightRightToMatrix_ρ_symm` 📖	mathematical	—	`rightHanded` `rightRightToMatrix`	—	`rightRightToMatrix_ρ`

---

← Back to Index