Documentation Verification Report

Pre

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

Statistics

Metric	Count
Definitions `preCoContrUnit`, `preCoContrUnitVal`, `preContrCoUnit`, `preContrCoUnitVal`	4
Theorems `contr_preCoContrUnit`, `contr_preContrCoUnit`, `preCoContrUnitVal_expand_tmul`, `preCoContrUnit_apply_one`, `preCoContrUnit_symm`, `preContrCoUnitVal_expand_tmul`, `preContrCoUnit_apply_one`, `preContrCoUnit_symm`	8
Total	12

Lorentz

Definitions

Name	Category	Theorems
`preCoContrUnit` 📖	CompOp	5 math math: `contr_preCoContrUnit`, `preCoContrUnit_symm`, `preCoContrUnit_apply_one`, `preContrCoUnit_symm`, `contrCoContract_apply_metric`
`preCoContrUnitVal` 📖	CompOp	2 math math: `preCoContrUnitVal_expand_tmul`, `preCoContrUnit_apply_one`
`preContrCoUnit` 📖	CompOp	5 math math: `coContrContract_apply_metric`, `preContrCoUnit_apply_one`, `contr_preContrCoUnit`, `preCoContrUnit_symm`, `preContrCoUnit_symm`
`preContrCoUnitVal` 📖	CompOp	2 math math: `preContrCoUnit_apply_one`, `preContrCoUnitVal_expand_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contr_preCoContrUnit` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `Co` `contrCoContract` `preCoContrUnit`	—	`preCoContrUnit_apply_one` `preCoContrUnitVal_expand_tmul` `contrCoContract_basis`
`contr_preContrCoUnit` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `Contr` `coContrContract` `preContrCoUnit`	—	`preContrCoUnit_apply_one` `preContrCoUnitVal_expand_tmul` `coContrContract_basis`
`preCoContrUnitVal_expand_tmul` 📖	mathematical	—	`preCoContrUnitVal` `LorentzGroup` `lorentzGroupIsGroup` `Co` `Contr` `coBasis` `contrBasis`	—	`coContrToMatrixRe_symm_expand_tmul`
`preCoContrUnit_apply_one` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `Contr` `preCoContrUnit` `preCoContrUnitVal`	—	—
`preCoContrUnit_symm` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `Contr` `preCoContrUnit` `preContrCoUnit`	—	`preContrCoUnit_apply_one` `preContrCoUnitVal_expand_tmul` `preCoContrUnit_apply_one` `preCoContrUnitVal_expand_tmul`
`preContrCoUnitVal_expand_tmul` 📖	mathematical	—	`preContrCoUnitVal` `LorentzGroup` `lorentzGroupIsGroup` `Contr` `Co` `contrBasis` `coBasis`	—	`contrCoToMatrixRe_symm_expand_tmul`
`preContrCoUnit_apply_one` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `Co` `preContrCoUnit` `preContrCoUnitVal`	—	—
`preContrCoUnit_symm` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `Co` `preContrCoUnit` `preCoContrUnit`	—	`preContrCoUnit_apply_one` `preContrCoUnitVal_expand_tmul` `preCoContrUnit_apply_one` `preCoContrUnitVal_expand_tmul`

---

← Back to Index