Documentation Verification Report

AsTensor

📁 Source: PhysLean/Relativity/PauliMatrices/AsTensor.lean

Statistics

Metric	Count
Definitions `asConsTensor`, `asTensor`	2
Theorems `asConsTensor_apply_one`, `asTensor_expand`, `asTensor_expand_complexContrBasis`, `leftRightToMatrix_σSA_inl_0_expand`, `leftRightToMatrix_σSA_inr_0_expand`, `leftRightToMatrix_σSA_inr_1_expand`, `leftRightToMatrix_σSA_inr_2_expand`	7
Total	9

PauliMatrix

Definitions

Name	Category	Theorems
`asConsTensor` 📖	CompOp	2 math math: `asConsTensor_apply_one`, `toTensor_eq_asConsTensor`
`asTensor` 📖	CompOp	3 math math: `asConsTensor_apply_one`, `asTensor_expand`, `asTensor_expand_complexContrBasis`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asConsTensor_apply_one` 📖	mathematical	—	`Lorentz.complexContr` `Fermion.leftHanded` `Fermion.rightHanded` `asConsTensor` `asTensor`	—	—
`asTensor_expand` 📖	mathematical	—	`asTensor` `Lorentz.complexContr` `Fermion.leftHanded` `Fermion.rightHanded` `Lorentz.complexContrBasis` `Fermion.leftBasis` `Fermion.rightBasis`	—	`asTensor_expand_complexContrBasis` `leftRightToMatrix_σSA_inl_0_expand` `leftRightToMatrix_σSA_inr_0_expand` `leftRightToMatrix_σSA_inr_1_expand` `leftRightToMatrix_σSA_inr_2_expand`
`asTensor_expand_complexContrBasis` 📖	mathematical	—	`asTensor` `Lorentz.complexContr` `Fermion.leftHanded` `Fermion.rightHanded` `Lorentz.complexContrBasis` `Fermion.leftRightToMatrix` `pauliBasis`	—	—
`leftRightToMatrix_σSA_inl_0_expand` 📖	mathematical	—	`Fermion.leftHanded` `Fermion.rightHanded` `Fermion.leftRightToMatrix` `pauliBasis` `Fermion.leftBasis` `Fermion.rightBasis`	—	`Fermion.leftRightToMatrix_symm_expand_tmul` `pauliSelfAdjoint_linearly_independent` `pauliSelfAdjoint_span`
`leftRightToMatrix_σSA_inr_0_expand` 📖	mathematical	—	`Fermion.leftHanded` `Fermion.rightHanded` `Fermion.leftRightToMatrix` `pauliBasis` `Fermion.leftBasis` `Fermion.rightBasis`	—	`Fermion.leftRightToMatrix_symm_expand_tmul` `pauliSelfAdjoint_linearly_independent` `pauliSelfAdjoint_span`
`leftRightToMatrix_σSA_inr_1_expand` 📖	mathematical	—	`Fermion.leftHanded` `Fermion.rightHanded` `Fermion.leftRightToMatrix` `pauliBasis` `Fermion.leftBasis` `Fermion.rightBasis`	—	`Fermion.leftRightToMatrix_symm_expand_tmul` `pauliSelfAdjoint_linearly_independent` `pauliSelfAdjoint_span`
`leftRightToMatrix_σSA_inr_2_expand` 📖	mathematical	—	`Fermion.leftHanded` `Fermion.rightHanded` `Fermion.leftRightToMatrix` `pauliBasis` `Fermion.leftBasis` `Fermion.rightBasis`	—	`Fermion.leftRightToMatrix_symm_expand_tmul` `pauliSelfAdjoint_linearly_independent` `pauliSelfAdjoint_span`

---

← Back to Index