Documentation Verification Report

Pre

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

Statistics

Metric	Count
Definitions `coMetric`, `coMetricVal`, `contrMetric`, `contrMetricVal`	4
Theorems `coContrContraction_apply_metric`, `coMetricVal_expand_tmul`, `coMetric_apply_one`, `contrCoContraction_apply_metric`, `contrMetricVal_expand_tmul`, `contrMetric_apply_one`	6
Total	10

Lorentz

Definitions

Name	Category	Theorems
`coMetric` 📖	CompOp	4 math math: `coContrContraction_apply_metric`, `complexLorentzTensor.coMetric_eq_fromConstPair`, `contrCoContraction_apply_metric`, `coMetric_apply_one`
`coMetricVal` 📖	CompOp	3 math math: `complexLorentzTensor.coMetric_eq_fromPairT`, `coMetricVal_expand_tmul`, `coMetric_apply_one`
`contrMetric` 📖	CompOp	4 math math: `coContrContraction_apply_metric`, `contrMetric_apply_one`, `complexLorentzTensor.contrMetric_eq_fromConstPair`, `contrCoContraction_apply_metric`
`contrMetricVal` 📖	CompOp	3 math math: `complexLorentzTensor.contrMetric_eq_fromPairT`, `contrMetricVal_expand_tmul`, `contrMetric_apply_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coContrContraction_apply_metric` 📖	mathematical	—	`complexCo` `complexContr` `coContrContraction` `coMetric` `contrMetric` `contrCoUnit`	—	`coMetric_apply_one` `contrMetric_apply_one` `coMetricVal_expand_tmul` `contrMetricVal_expand_tmul` `coContrContraction_basis'` `contrCoUnit_apply_one` `contrCoUnitVal_expand_tmul`
`coMetricVal_expand_tmul` 📖	mathematical	—	`coMetricVal` `complexCo` `complexCoBasis`	—	`coCoToMatrix_symm_expand_tmul` `minkowskiMatrix.off_diag_zero` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i`
`coMetric_apply_one` 📖	mathematical	—	`complexCo` `coMetric` `coMetricVal`	—	—
`contrCoContraction_apply_metric` 📖	mathematical	—	`complexContr` `complexCo` `contrCoContraction` `contrMetric` `coMetric` `coContrUnit`	—	`contrMetric_apply_one` `coMetric_apply_one` `contrMetricVal_expand_tmul` `coMetricVal_expand_tmul` `contrCoContraction_basis'` `coContrUnit_apply_one` `coContrUnitVal_expand_tmul`
`contrMetricVal_expand_tmul` 📖	mathematical	—	`contrMetricVal` `complexContr` `complexContrBasis`	—	`contrContrToMatrix_symm_expand_tmul` `minkowskiMatrix.off_diag_zero` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i`
`contrMetric_apply_one` 📖	mathematical	—	`complexContr` `contrMetric` `contrMetricVal`	—	—

---

← Back to Index