Documentation Verification Report

Pre

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

Statistics

Metric	Count
Definitions `preCoMetric`, `preCoMetricVal`, `preContrMetric`, `preContrMetricVal`	4
Theorems `coContrContract_apply_metric`, `contrCoContract_apply_metric`, `preCoMetricVal_expand_tmul`, `preCoMetricVal_expand_tmul_minkowskiMatrix`, `preCoMetric_apply_one`, `preContrMetricVal_expand_tmul`, `preContrMetricVal_expand_tmul_minkowskiMatrix`, `preContrMetric_apply_one`	8
Total	12

Lorentz

Definitions

Name	Category	Theorems
`preCoMetric` 📖	CompOp	4 math math: `coContrContract_apply_metric`, `realLorentzTensor.coMetric_eq_fromConstPair`, `preCoMetric_apply_one`, `contrCoContract_apply_metric`
`preCoMetricVal` 📖	CompOp	4 math math: `preCoMetricVal_expand_tmul`, `preCoMetric_apply_one`, `realLorentzTensor.coMetric_eq_fromPairT`, `preCoMetricVal_expand_tmul_minkowskiMatrix`
`preContrMetric` 📖	CompOp	4 math math: `coContrContract_apply_metric`, `realLorentzTensor.contrMetric_eq_fromConstPair`, `preContrMetric_apply_one`, `contrCoContract_apply_metric`
`preContrMetricVal` 📖	CompOp	4 math math: `preContrMetricVal_expand_tmul_minkowskiMatrix`, `realLorentzTensor.contrMetric_eq_fromPairT`, `preContrMetricVal_expand_tmul`, `preContrMetric_apply_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coContrContract_apply_metric` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `Contr` `coContrContract` `preCoMetric` `preContrMetric` `preContrCoUnit`	—	`preCoMetric_apply_one` `preContrMetric_apply_one` `preCoMetricVal_expand_tmul_minkowskiMatrix` `preContrMetricVal_expand_tmul_minkowskiMatrix` `coContrContract_basis` `minkowskiMatrix.η_apply_mul_η_apply_diag` `preContrCoUnit_apply_one` `preContrCoUnitVal_expand_tmul`
`contrCoContract_apply_metric` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `Co` `contrCoContract` `preContrMetric` `preCoMetric` `preCoContrUnit`	—	`preContrMetric_apply_one` `preCoMetric_apply_one` `preContrMetricVal_expand_tmul_minkowskiMatrix` `preCoMetricVal_expand_tmul_minkowskiMatrix` `contrCoContract_basis` `minkowskiMatrix.η_apply_mul_η_apply_diag` `preCoContrUnit_apply_one` `preCoContrUnitVal_expand_tmul`
`preCoMetricVal_expand_tmul` 📖	mathematical	—	`preCoMetricVal` `LorentzGroup` `lorentzGroupIsGroup` `Co` `coBasis`	—	`coCoToMatrixRe_symm_expand_tmul` `minkowskiMatrix.off_diag_zero` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i`
`preCoMetricVal_expand_tmul_minkowskiMatrix` 📖	mathematical	—	`preCoMetricVal` `LorentzGroup` `lorentzGroupIsGroup` `Co` `minkowskiMatrix` `coBasis`	—	`preCoMetricVal_expand_tmul` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i`
`preCoMetric_apply_one` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `preCoMetric` `preCoMetricVal`	—	—
`preContrMetricVal_expand_tmul` 📖	mathematical	—	`preContrMetricVal` `LorentzGroup` `lorentzGroupIsGroup` `Contr` `contrBasis`	—	`contrContrToMatrixRe_symm_expand_tmul` `minkowskiMatrix.off_diag_zero` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i`
`preContrMetricVal_expand_tmul_minkowskiMatrix` 📖	mathematical	—	`preContrMetricVal` `LorentzGroup` `lorentzGroupIsGroup` `Contr` `minkowskiMatrix` `contrBasis`	—	`preContrMetricVal_expand_tmul` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i`
`preContrMetric_apply_one` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `preContrMetric` `preContrMetricVal`	—	—

---

← Back to Index