Documentation Verification Report

Pre

📁 Source: PhysLean/Relativity/Tensors/ComplexTensor/Units/Pre.lean

Statistics

Metric	Count
Definitions `coContrUnit`, `coContrUnitVal`, `contrCoUnit`, `contrCoUnitVal`	4
Theorems `coContrUnitVal_expand_tmul`, `coContrUnit_apply_one`, `coContrUnit_symm`, `contrCoUnitVal_expand_tmul`, `contrCoUnit_apply_one`, `contrCoUnit_symm`, `contr_coContrUnit`, `contr_contrCoUnit`	8
Total	12

Lorentz

Definitions

Name	Category	Theorems
`coContrUnit` 📖	CompOp	6 math math: `contr_coContrUnit`, `coContrUnit_symm`, `contrCoUnit_symm`, `complexLorentzTensor.coContrUnit_eq_fromConstPair`, `contrCoContraction_apply_metric`, `coContrUnit_apply_one`
`coContrUnitVal` 📖	CompOp	3 math math: `complexLorentzTensor.coContrUnit_eq_fromPairT`, `coContrUnitVal_expand_tmul`, `coContrUnit_apply_one`
`contrCoUnit` 📖	CompOp	6 math math: `coContrUnit_symm`, `contrCoUnit_symm`, `complexLorentzTensor.contrCoUnit_eq_fromConstPair`, `coContrContraction_apply_metric`, `contrCoUnit_apply_one`, `contr_contrCoUnit`
`contrCoUnitVal` 📖	CompOp	3 math math: `contrCoUnitVal_expand_tmul`, `complexLorentzTensor.contrCoUnit_eq_fromPairT`, `contrCoUnit_apply_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coContrUnitVal_expand_tmul` 📖	mathematical	—	`coContrUnitVal` `complexCo` `complexContr` `complexCoBasis` `complexContrBasis`	—	`coContrToMatrix_symm_expand_tmul`
`coContrUnit_apply_one` 📖	mathematical	—	`complexCo` `complexContr` `coContrUnit` `coContrUnitVal`	—	—
`coContrUnit_symm` 📖	mathematical	—	`complexCo` `complexContr` `coContrUnit` `contrCoUnit`	—	`coContrUnit_apply_one` `coContrUnitVal_expand_tmul` `contrCoUnit_apply_one` `contrCoUnitVal_expand_tmul`
`contrCoUnitVal_expand_tmul` 📖	mathematical	—	`contrCoUnitVal` `complexContr` `complexCo` `complexContrBasis` `complexCoBasis`	—	`contrCoToMatrix_symm_expand_tmul`
`contrCoUnit_apply_one` 📖	mathematical	—	`complexContr` `complexCo` `contrCoUnit` `contrCoUnitVal`	—	—
`contrCoUnit_symm` 📖	mathematical	—	`complexContr` `complexCo` `contrCoUnit` `coContrUnit`	—	`contrCoUnit_apply_one` `contrCoUnitVal_expand_tmul` `coContrUnit_apply_one` `coContrUnitVal_expand_tmul`
`contr_coContrUnit` 📖	mathematical	—	`complexContr` `complexCo` `contrCoContraction` `coContrUnit`	—	`coContrUnit_apply_one` `coContrUnitVal_expand_tmul` `contrCoContraction_basis'`
`contr_contrCoUnit` 📖	mathematical	—	`complexCo` `complexContr` `coContrContraction` `contrCoUnit`	—	`contrCoUnit_apply_one` `contrCoUnitVal_expand_tmul` `coContrContraction_basis'`

---

← Back to Index