Documentation Verification Report

Contraction

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

Statistics

Metric	Count
Definitions `altLeftBi`, `altLeftContraction`, `altRightBi`, `altRightContraction`, `leftAltBi`, `leftAltContraction`, `rightAltBi`, `rightAltContraction`	8
Theorems `altLeftContraction_basis`, `altLeftContraction_hom_tmul`, `altLeftContraction_tmul_symm`, `altRightContraction_basis`, `altRightContraction_hom_tmul`, `altRightContraction_tmul_symm`, `leftAltContraction_basis`, `leftAltContraction_hom_tmul`, `leftAltContraction_tmul_symm`, `rightAltContraction_basis`, `rightAltContraction_hom_tmul`, `rightAltContraction_tmul_symm`	12
Total	20

Fermion

Definitions

Name	Category	Theorems
`altLeftBi` 📖	CompOp	—
`altLeftContraction` 📖	CompOp	6 math math: `altLeftContraction_basis`, `leftAltContraction_tmul_symm`, `altLeftContraction_hom_tmul`, `contr_leftAltLeftUnit`, `altLeftContraction_apply_metric`, `altLeftContraction_tmul_symm`
`altRightBi` 📖	CompOp	—
`altRightContraction` 📖	CompOp	6 math math: `altRightContraction_hom_tmul`, `contr_rightAltRightUnit`, `altRightContraction_basis`, `altRightContraction_tmul_symm`, `rightAltContraction_tmul_symm`, `altRightContraction_apply_metric`
`leftAltBi` 📖	CompOp	—
`leftAltContraction` 📖	CompOp	6 math math: `leftAltContraction_tmul_symm`, `leftAltContraction_basis`, `contr_altLeftLeftUnit`, `altLeftContraction_tmul_symm`, `leftAltContraction_apply_metric`, `leftAltContraction_hom_tmul`
`rightAltBi` 📖	CompOp	—
`rightAltContraction` 📖	CompOp	6 math math: `rightAltContraction_basis`, `contr_altRightRightUnit`, `rightAltContraction_hom_tmul`, `rightAltContraction_apply_metric`, `altRightContraction_tmul_symm`, `rightAltContraction_tmul_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`altLeftContraction_basis` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftContraction` `altLeftBasis` `leftBasis`	—	`altLeftContraction_hom_tmul` `altLeftBasis_toFin2ℂ` `leftBasis_toFin2ℂ`
`altLeftContraction_hom_tmul` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftContraction` `AltLeftHandedModule.toFin2ℂ` `LeftHandedModule.toFin2ℂ`	—	—
`altLeftContraction_tmul_symm` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftContraction` `leftAltContraction`	—	`leftAltContraction_tmul_symm`
`altRightContraction_basis` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightContraction` `altRightBasis` `rightBasis`	—	`altRightContraction_hom_tmul` `altRightBasis_toFin2ℂ` `rightBasis_toFin2ℂ`
`altRightContraction_hom_tmul` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightContraction` `AltRightHandedModule.toFin2ℂ` `RightHandedModule.toFin2ℂ`	—	—
`altRightContraction_tmul_symm` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightContraction` `rightAltContraction`	—	`rightAltContraction_tmul_symm`
`leftAltContraction_basis` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltContraction` `leftBasis` `altLeftBasis`	—	`leftAltContraction_hom_tmul` `leftBasis_toFin2ℂ` `altLeftBasis_toFin2ℂ`
`leftAltContraction_hom_tmul` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltContraction` `LeftHandedModule.toFin2ℂ` `AltLeftHandedModule.toFin2ℂ`	—	—
`leftAltContraction_tmul_symm` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltContraction` `altLeftContraction`	—	`leftAltContraction_hom_tmul` `altLeftContraction_hom_tmul`
`rightAltContraction_basis` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltContraction` `rightBasis` `altRightBasis`	—	`rightAltContraction_hom_tmul` `rightBasis_toFin2ℂ` `altRightBasis_toFin2ℂ`
`rightAltContraction_hom_tmul` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltContraction` `RightHandedModule.toFin2ℂ` `AltRightHandedModule.toFin2ℂ`	—	—
`rightAltContraction_tmul_symm` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltContraction` `altRightContraction`	—	`rightAltContraction_hom_tmul` `altRightContraction_hom_tmul`

---

← Back to Index