Documentation Verification Report

Unit

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

Statistics

Metric	Count
Definitions `altLeftLeftUnit`, `altLeftLeftUnitVal`, `altRightRightUnit`, `altRightRightUnitVal`, `leftAltLeftUnit`, `leftAltLeftUnitVal`, `rightAltRightUnit`, `rightAltRightUnitVal`	8
Theorems `altLeftLeftUnitVal_expand_tmul`, `altLeftLeftUnit_apply_one`, `altLeftLeftUnit_symm`, `altRightRightUnitVal_expand_tmul`, `altRightRightUnit_apply_one`, `altRightRightUnit_symm`, `contr_altLeftLeftUnit`, `contr_altRightRightUnit`, `contr_leftAltLeftUnit`, `contr_rightAltRightUnit`, `leftAltLeftUnitVal_expand_tmul`, `leftAltLeftUnit_apply_one`, `leftAltLeftUnit_symm`, `rightAltRightUnitVal_expand_tmul`, `rightAltRightUnit_apply_one`, `rightAltRightUnit_symm`	16
Total	24

Fermion

Definitions

Name	Category	Theorems
`altLeftLeftUnit` 📖	CompOp	6 math math: `altLeftLeftUnit_apply_one`, `contr_altLeftLeftUnit`, `leftAltLeftUnit_symm`, `leftAltContraction_apply_metric`, `altLeftLeftUnit_symm`, `complexLorentzTensor.altLeftLeftUnit_eq_fromConstPair`
`altLeftLeftUnitVal` 📖	CompOp	3 math math: `altLeftLeftUnit_apply_one`, `altLeftLeftUnitVal_expand_tmul`, `complexLorentzTensor.altLeftLeftUnit_eq_fromPairT`
`altRightRightUnit` 📖	CompOp	6 math math: `complexLorentzTensor.altRightRightUnit_eq_fromConstPair`, `contr_altRightRightUnit`, `altRightRightUnit_symm`, `rightAltContraction_apply_metric`, `rightAltRightUnit_symm`, `altRightRightUnit_apply_one`
`altRightRightUnitVal` 📖	CompOp	3 math math: `complexLorentzTensor.altRightRightUnit_eq_fromPairT`, `altRightRightUnit_apply_one`, `altRightRightUnitVal_expand_tmul`
`leftAltLeftUnit` 📖	CompOp	6 math math: `leftAltLeftUnit_apply_one`, `contr_leftAltLeftUnit`, `complexLorentzTensor.leftAltLeftUnit_eq_fromConstPair`, `altLeftContraction_apply_metric`, `leftAltLeftUnit_symm`, `altLeftLeftUnit_symm`
`leftAltLeftUnitVal` 📖	CompOp	3 math math: `complexLorentzTensor.leftAltLeftUnit_eq_fromPairT`, `leftAltLeftUnit_apply_one`, `leftAltLeftUnitVal_expand_tmul`
`rightAltRightUnit` 📖	CompOp	6 math math: `altRightRightUnit_symm`, `complexLorentzTensor.rightAltRightUnit_eq_fromConstPair`, `rightAltRightUnit_symm`, `contr_rightAltRightUnit`, `rightAltRightUnit_apply_one`, `altRightContraction_apply_metric`
`rightAltRightUnitVal` 📖	CompOp	3 math math: `complexLorentzTensor.rightAltRightUnit_eq_fromPairT`, `rightAltRightUnitVal_expand_tmul`, `rightAltRightUnit_apply_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`altLeftLeftUnitVal_expand_tmul` 📖	mathematical	—	`altLeftLeftUnitVal` `altLeftHanded` `leftHanded` `altLeftBasis` `leftBasis`	—	`altLeftLeftToMatrix_symm_expand_tmul`
`altLeftLeftUnit_apply_one` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftLeftUnit` `altLeftLeftUnitVal`	—	—
`altLeftLeftUnit_symm` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftLeftUnit` `leftAltLeftUnit`	—	`altLeftLeftUnit_apply_one` `altLeftLeftUnitVal_expand_tmul` `leftAltLeftUnit_apply_one` `leftAltLeftUnitVal_expand_tmul`
`altRightRightUnitVal_expand_tmul` 📖	mathematical	—	`altRightRightUnitVal` `altRightHanded` `rightHanded` `altRightBasis` `rightBasis`	—	`altRightRightToMatrix_symm_expand_tmul`
`altRightRightUnit_apply_one` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightRightUnit` `altRightRightUnitVal`	—	—
`altRightRightUnit_symm` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightRightUnit` `rightAltRightUnit`	—	`altRightRightUnit_apply_one` `altRightRightUnitVal_expand_tmul` `rightAltRightUnit_apply_one` `rightAltRightUnitVal_expand_tmul`
`contr_altLeftLeftUnit` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltContraction` `altLeftLeftUnit`	—	`altLeftLeftUnit_apply_one` `altLeftLeftUnitVal_expand_tmul` `leftAltContraction_basis`
`contr_altRightRightUnit` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltContraction` `altRightRightUnit`	—	`altRightRightUnit_apply_one` `altRightRightUnitVal_expand_tmul` `rightAltContraction_basis`
`contr_leftAltLeftUnit` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftContraction` `leftAltLeftUnit`	—	`leftAltLeftUnit_apply_one` `leftAltLeftUnitVal_expand_tmul` `altLeftContraction_basis`
`contr_rightAltRightUnit` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightContraction` `rightAltRightUnit`	—	`rightAltRightUnit_apply_one` `rightAltRightUnitVal_expand_tmul` `altRightContraction_basis`
`leftAltLeftUnitVal_expand_tmul` 📖	mathematical	—	`leftAltLeftUnitVal` `leftHanded` `altLeftHanded` `leftBasis` `altLeftBasis`	—	`leftAltLeftToMatrix_symm_expand_tmul`
`leftAltLeftUnit_apply_one` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltLeftUnit` `leftAltLeftUnitVal`	—	—
`leftAltLeftUnit_symm` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltLeftUnit` `altLeftLeftUnit`	—	`altLeftLeftUnit_apply_one` `altLeftLeftUnitVal_expand_tmul` `leftAltLeftUnit_apply_one` `leftAltLeftUnitVal_expand_tmul`
`rightAltRightUnitVal_expand_tmul` 📖	mathematical	—	`rightAltRightUnitVal` `rightHanded` `altRightHanded` `rightBasis` `altRightBasis`	—	`rightAltRightToMatrix_symm_expand_tmul`
`rightAltRightUnit_apply_one` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltRightUnit` `rightAltRightUnitVal`	—	—
`rightAltRightUnit_symm` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltRightUnit` `altRightRightUnit`	—	`altRightRightUnit_apply_one` `altRightRightUnitVal_expand_tmul` `rightAltRightUnit_apply_one` `rightAltRightUnitVal_expand_tmul`

---

← Back to Index