Documentation Verification Report

Contraction

📁 Source: PhysLean/Relativity/Tensors/ComplexTensor/Vector/Pre/Contraction.lean

Statistics

Metric	Count
Definitions `coContrContraction`, `contrCoContrBi`, `contrCoContraction`, `contrContrCoBi`	4
Theorems `coContrContraction_basis`, `coContrContraction_basis'`, `coContrContraction_hom_tmul`, `coContrContraction_tmul_symm`, `contrCoContraction_basis`, `contrCoContraction_basis'`, `contrCoContraction_hom_tmul`, `contrCoContraction_tmul_symm`	8
Total	12

Lorentz

Definitions

Name	Category	Theorems
`coContrContraction` 📖	CompOp	7 math math: `coContrContraction_apply_metric`, `contrCoContraction_tmul_symm`, `coContrContraction_basis'`, `coContrContraction_hom_tmul`, `coContrContraction_basis`, `coContrContraction_tmul_symm`, `contr_contrCoUnit`
`contrCoContrBi` 📖	CompOp	—
`contrCoContraction` 📖	CompOp	7 math math: `contrCoContraction_basis`, `contr_coContrUnit`, `contrCoContraction_basis'`, `contrCoContraction_hom_tmul`, `contrCoContraction_tmul_symm`, `contrCoContraction_apply_metric`, `coContrContraction_tmul_symm`
`contrContrCoBi` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coContrContraction_basis` 📖	mathematical	—	`complexCo` `complexContr` `coContrContraction` `complexCoBasisFin4` `complexContrBasisFin4`	—	`coContrContraction_hom_tmul` `complexCoBasis_toFin13ℂ` `complexContrBasis_toFin13ℂ`
`coContrContraction_basis'` 📖	mathematical	—	`complexCo` `complexContr` `coContrContraction` `complexCoBasis` `complexContrBasis`	—	`coContrContraction_hom_tmul` `complexCoBasis_toFin13ℂ` `complexContrBasis_toFin13ℂ`
`coContrContraction_hom_tmul` 📖	mathematical	—	`complexCo` `complexContr` `coContrContraction` `CoℂModule.toFin13ℂ` `ContrℂModule.toFin13ℂ`	—	—
`coContrContraction_tmul_symm` 📖	mathematical	—	`complexCo` `complexContr` `coContrContraction` `contrCoContraction`	—	`contrCoContraction_tmul_symm`
`contrCoContraction_basis` 📖	mathematical	—	`complexContr` `complexCo` `contrCoContraction` `complexContrBasisFin4` `complexCoBasisFin4`	—	`contrCoContraction_hom_tmul` `complexContrBasis_toFin13ℂ` `complexCoBasis_toFin13ℂ`
`contrCoContraction_basis'` 📖	mathematical	—	`complexContr` `complexCo` `contrCoContraction` `complexContrBasis` `complexCoBasis`	—	`contrCoContraction_hom_tmul` `complexContrBasis_toFin13ℂ` `complexCoBasis_toFin13ℂ`
`contrCoContraction_hom_tmul` 📖	mathematical	—	`complexContr` `complexCo` `contrCoContraction` `ContrℂModule.toFin13ℂ` `CoℂModule.toFin13ℂ`	—	—
`contrCoContraction_tmul_symm` 📖	mathematical	—	`complexContr` `complexCo` `contrCoContraction` `coContrContraction`	—	`contrCoContraction_hom_tmul` `coContrContraction_hom_tmul`

---

← Back to Index