Documentation Verification Report

Pre

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

Statistics

Metric	Count
Definitions `coCoToMatrix`, `coContrToMatrix`, `contrCoToMatrix`, `contrContrToMatrix`	4
Theorems `coCoToMatrix_symm_expand_tmul`, `coCoToMatrix_ρ`, `coCoToMatrix_ρ_symm`, `coContrToMatrix_symm_expand_tmul`, `coContrToMatrix_ρ`, `coContrToMatrix_ρ_symm`, `contrCoToMatrix_symm_expand_tmul`, `contrCoToMatrix_ρ`, `contrCoToMatrix_ρ_symm`, `contrContrToMatrix_symm_expand_tmul`, `contrContrToMatrix_ρ`, `contrContrToMatrix_ρ_symm`	12
Total	16

Lorentz

Definitions

Name	Category	Theorems
`coCoToMatrix` 📖	CompOp	3 math math: `coCoToMatrix_symm_expand_tmul`, `coCoToMatrix_ρ`, `coCoToMatrix_ρ_symm`
`coContrToMatrix` 📖	CompOp	3 math math: `coContrToMatrix_ρ`, `coContrToMatrix_symm_expand_tmul`, `coContrToMatrix_ρ_symm`
`contrCoToMatrix` 📖	CompOp	3 math math: `contrCoToMatrix_ρ_symm`, `contrCoToMatrix_ρ`, `contrCoToMatrix_symm_expand_tmul`
`contrContrToMatrix` 📖	CompOp	3 math math: `contrContrToMatrix_ρ_symm`, `contrContrToMatrix_symm_expand_tmul`, `contrContrToMatrix_ρ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coCoToMatrix_symm_expand_tmul` 📖	mathematical	—	`complexCo` `coCoToMatrix` `complexCoBasis`	—	—
`coCoToMatrix_ρ` 📖	mathematical	—	`complexCo` `coCoToMatrix` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	`coCoToMatrix.eq_1` `complexCoBasis_ρ_apply`
`coCoToMatrix_ρ_symm` 📖	mathematical	—	`complexCo` `coCoToMatrix` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	`coCoToMatrix_ρ`
`coContrToMatrix_symm_expand_tmul` 📖	mathematical	—	`complexCo` `complexContr` `coContrToMatrix` `complexCoBasis` `complexContrBasis`	—	—
`coContrToMatrix_ρ` 📖	mathematical	—	`complexCo` `complexContr` `coContrToMatrix` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	`coContrToMatrix.eq_1` `complexCoBasis_ρ_apply` `complexContrBasis_ρ_apply`
`coContrToMatrix_ρ_symm` 📖	mathematical	—	`complexCo` `complexContr` `coContrToMatrix` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	`coContrToMatrix_ρ`
`contrCoToMatrix_symm_expand_tmul` 📖	mathematical	—	`complexContr` `complexCo` `contrCoToMatrix` `complexContrBasis` `complexCoBasis`	—	—
`contrCoToMatrix_ρ` 📖	mathematical	—	`complexContr` `complexCo` `contrCoToMatrix` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	`contrCoToMatrix.eq_1` `complexContrBasis_ρ_apply` `complexCoBasis_ρ_apply`
`contrCoToMatrix_ρ_symm` 📖	mathematical	—	`complexContr` `complexCo` `contrCoToMatrix` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	`contrCoToMatrix_ρ`
`contrContrToMatrix_symm_expand_tmul` 📖	mathematical	—	`complexContr` `contrContrToMatrix` `complexContrBasis`	—	—
`contrContrToMatrix_ρ` 📖	mathematical	—	`complexContr` `contrContrToMatrix` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	`contrContrToMatrix.eq_1` `complexContrBasis_ρ_apply`
`contrContrToMatrix_ρ_symm` 📖	mathematical	—	`complexContr` `contrContrToMatrix` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	`contrContrToMatrix_ρ`

---

← Back to Index