Documentation Verification Report

Basic

📁 Source: PhysLean/Relativity/Tensors/ComplexTensor/Vector/Pre/Basic.lean

Statistics

Metric	Count
Definitions `complexCo`, `complexCoBasis`, `complexCoBasisFin4`, `complexContr`, `complexContrBasis`, `complexContrBasisFin4`, `inclCongrRealLorentz`	7
Theorems `SL2CRep_ρ_basis`, `complexCoBasisFin4_apply_one`, `complexCoBasisFin4_apply_three`, `complexCoBasisFin4_apply_two`, `complexCoBasisFin4_apply_zero`, `complexCoBasis_toFin13ℂ`, `complexCoBasis_ρ_apply`, `complexContrBasisFin4_apply_one`, `complexContrBasisFin4_apply_succ`, `complexContrBasisFin4_apply_three`, `complexContrBasisFin4_apply_two`, `complexContrBasisFin4_apply_zero`, `complexContrBasis_of_real`, `complexContrBasis_toFin13ℂ`, `complexContrBasis_ρ_apply`, `complexContrBasis_ρ_val`, `inclCongrRealLorentz_val`, `inclCongrRealLorentz_ρ`	18
Total	25

Lorentz

Definitions

Name	Category	Theorems
`complexCo` 📖	CompOp	42 math math: `contrCoContraction_basis`, `contr_coContrUnit`, `complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis`, `complexCoBasisFin4_apply_one`, `coContrUnit_symm`, `contrCoUnit_symm`, `coCoToMatrix_symm_expand_tmul`, `contrCoUnitVal_expand_tmul`, `coContrToMatrix_ρ`, `contrCoContraction_basis'`, `coContrContraction_apply_metric`, `complexCoBasis_toFin13ℂ`, `complexCoBasis_ρ_apply`, `complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4`, `coCoToMatrix_ρ`, `complexCoBasisFin4_apply_three`, `coContrToMatrix_symm_expand_tmul`, `contrCoContraction_hom_tmul`, `complexLorentzTensor.basis_down_eq`, `contrCoContraction_tmul_symm`, `coContrContraction_basis'`, `coContrContraction_hom_tmul`, `coCoToMatrix_ρ_symm`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4`, `contrCoToMatrix_ρ_symm`, `coContrContraction_basis`, `complexLorentzTensor.coMetric_eq_complexCoBasisFin4`, `coContrUnitVal_expand_tmul`, `contrCoToMatrix_ρ`, `complexLorentzTensor.coMetric_eq_complexCoBasis`, `complexCoBasisFin4_apply_two`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis`, `coContrToMatrix_ρ_symm`, `contrCoContraction_apply_metric`, `coMetricVal_expand_tmul`, `contrCoUnit_apply_one`, `coContrUnit_apply_one`, `coContrContraction_tmul_symm`, `contr_contrCoUnit`, `contrCoToMatrix_symm_expand_tmul`, `coMetric_apply_one`, `complexCoBasisFin4_apply_zero`
`complexCoBasis` 📖	CompOp	17 math math: `complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis`, `complexCoBasisFin4_apply_one`, `coCoToMatrix_symm_expand_tmul`, `contrCoUnitVal_expand_tmul`, `contrCoContraction_basis'`, `complexCoBasis_toFin13ℂ`, `complexCoBasis_ρ_apply`, `complexCoBasisFin4_apply_three`, `coContrToMatrix_symm_expand_tmul`, `coContrContraction_basis'`, `coContrUnitVal_expand_tmul`, `complexLorentzTensor.coMetric_eq_complexCoBasis`, `complexCoBasisFin4_apply_two`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis`, `coMetricVal_expand_tmul`, `contrCoToMatrix_symm_expand_tmul`, `complexCoBasisFin4_apply_zero`
`complexCoBasisFin4` 📖	CompOp	10 math math: `contrCoContraction_basis`, `complexCoBasisFin4_apply_one`, `complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4`, `complexCoBasisFin4_apply_three`, `complexLorentzTensor.basis_down_eq`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4`, `coContrContraction_basis`, `complexLorentzTensor.coMetric_eq_complexCoBasisFin4`, `complexCoBasisFin4_apply_two`, `complexCoBasisFin4_apply_zero`
`complexContr` 📖	CompOp	51 math math: `contrCoContraction_basis`, `complexContrBasis_toFin13ℂ`, `contr_coContrUnit`, `complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis`, `contrContrToMatrix_ρ_symm`, `contrContrToMatrix_symm_expand_tmul`, `coContrUnit_symm`, `complexContrBasis_ρ_apply`, `contrCoUnit_symm`, `complexContrBasisFin4_apply_three`, `contrCoUnitVal_expand_tmul`, `coContrToMatrix_ρ`, `SL2CRep_ρ_basis`, `complexLorentzTensor.basis_up_eq`, `complexLorentzTensor.contrMetric_eq_complexContrBasisFin4`, `inclCongrRealLorentz_ρ`, `contrCoContraction_basis'`, `complexLorentzTensor.contrMetric_eq_complexContrBasis`, `coContrContraction_apply_metric`, `complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4`, `PauliMatrix.asConsTensor_apply_one`, `coContrToMatrix_symm_expand_tmul`, `contrMetricVal_expand_tmul`, `complexContrBasisFin4_apply_succ`, `contrCoContraction_hom_tmul`, `PauliMatrix.asTensor_expand`, `contrCoContraction_tmul_symm`, `coContrContraction_basis'`, `coContrContraction_hom_tmul`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4`, `contrCoToMatrix_ρ_symm`, `coContrContraction_basis`, `inclCongrRealLorentz_val`, `complexContrBasisFin4_apply_one`, `contrMetric_apply_one`, `coContrUnitVal_expand_tmul`, `contrCoToMatrix_ρ`, `PauliMatrix.asTensor_expand_complexContrBasis`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis`, `complexContrBasis_ρ_val`, `complexContrBasisFin4_apply_zero`, `coContrToMatrix_ρ_symm`, `complexContrBasis_of_real`, `contrCoContraction_apply_metric`, `contrCoUnit_apply_one`, `coContrUnit_apply_one`, `coContrContraction_tmul_symm`, `contrContrToMatrix_ρ`, `contr_contrCoUnit`, `contrCoToMatrix_symm_expand_tmul`, `complexContrBasisFin4_apply_two`
`complexContrBasis` 📖	CompOp	22 math math: `complexContrBasis_toFin13ℂ`, `complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis`, `contrContrToMatrix_symm_expand_tmul`, `complexContrBasis_ρ_apply`, `complexContrBasisFin4_apply_three`, `contrCoUnitVal_expand_tmul`, `SL2CRep_ρ_basis`, `contrCoContraction_basis'`, `complexLorentzTensor.contrMetric_eq_complexContrBasis`, `coContrToMatrix_symm_expand_tmul`, `contrMetricVal_expand_tmul`, `complexContrBasisFin4_apply_succ`, `PauliMatrix.asTensor_expand`, `coContrContraction_basis'`, `complexContrBasisFin4_apply_one`, `coContrUnitVal_expand_tmul`, `PauliMatrix.asTensor_expand_complexContrBasis`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis`, `complexContrBasisFin4_apply_zero`, `complexContrBasis_of_real`, `contrCoToMatrix_symm_expand_tmul`, `complexContrBasisFin4_apply_two`
`complexContrBasisFin4` 📖	CompOp	11 math math: `contrCoContraction_basis`, `complexContrBasisFin4_apply_three`, `complexLorentzTensor.basis_up_eq`, `complexLorentzTensor.contrMetric_eq_complexContrBasisFin4`, `complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4`, `complexContrBasisFin4_apply_succ`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4`, `coContrContraction_basis`, `complexContrBasisFin4_apply_one`, `complexContrBasisFin4_apply_zero`, `complexContrBasisFin4_apply_two`
`inclCongrRealLorentz` 📖	CompOp	3 math math: `inclCongrRealLorentz_ρ`, `inclCongrRealLorentz_val`, `complexContrBasis_of_real`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SL2CRep_ρ_basis` 📖	mathematical	—	`complexContr` `complexContrBasis` `LorentzGroup` `lorentzGroupIsGroup` `SL2C.toLorentzGroup`	—	`complexContrBasis_of_real` `inclCongrRealLorentz_ρ` `Contr.ρ_stdBasis`
`complexCoBasisFin4_apply_one` 📖	mathematical	—	`complexCo` `complexCoBasisFin4` `complexCoBasis`	—	—
`complexCoBasisFin4_apply_three` 📖	mathematical	—	`complexCo` `complexCoBasisFin4` `complexCoBasis`	—	—
`complexCoBasisFin4_apply_two` 📖	mathematical	—	`complexCo` `complexCoBasisFin4` `complexCoBasis`	—	—
`complexCoBasisFin4_apply_zero` 📖	mathematical	—	`complexCo` `complexCoBasisFin4` `complexCoBasis`	—	—
`complexCoBasis_toFin13ℂ` 📖	mathematical	—	`CoℂModule.toFin13ℂ` `complexCo` `complexCoBasis`	—	—
`complexCoBasis_ρ_apply` 📖	mathematical	—	`complexCo` `complexCoBasis` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	—
`complexContrBasisFin4_apply_one` 📖	mathematical	—	`complexContr` `complexContrBasisFin4` `complexContrBasis`	—	—
`complexContrBasisFin4_apply_succ` 📖	mathematical	—	`complexContr` `complexContrBasisFin4` `complexContrBasis`	—	—
`complexContrBasisFin4_apply_three` 📖	mathematical	—	`complexContr` `complexContrBasisFin4` `complexContrBasis`	—	—
`complexContrBasisFin4_apply_two` 📖	mathematical	—	`complexContr` `complexContrBasisFin4` `complexContrBasis`	—	—
`complexContrBasisFin4_apply_zero` 📖	mathematical	—	`complexContr` `complexContrBasisFin4` `complexContrBasis`	—	—
`complexContrBasis_of_real` 📖	mathematical	—	`complexContr` `complexContrBasis` `ContrMod` `ContrMod.instAddCommMonoid` `ContrMod.instModuleReal` `inclCongrRealLorentz` `ContrMod.stdBasis`	—	`ContrℂModule.ext` `ContrMod.toFin1dℝ.eq_1` `ContrMod.stdBasis_toFin1dℝEquiv_apply_same` `ContrMod.stdBasis_toFin1dℝEquiv_apply_ne`
`complexContrBasis_toFin13ℂ` 📖	mathematical	—	`ContrℂModule.toFin13ℂ` `complexContr` `complexContrBasis`	—	—
`complexContrBasis_ρ_apply` 📖	mathematical	—	`complexContr` `complexContrBasis` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	—
`complexContrBasis_ρ_val` 📖	mathematical	—	`ContrℂModule.val` `complexContr` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `SL2C.toLorentzGroup`	—	—
`inclCongrRealLorentz_val` 📖	mathematical	—	`ContrℂModule.val` `ContrMod` `complexContr` `ContrMod.instAddCommMonoid` `ContrMod.instModuleReal` `inclCongrRealLorentz` `ContrMod.toFin1dℝ`	—	—
`inclCongrRealLorentz_ρ` 📖	mathematical	—	`complexContr` `ContrMod` `ContrMod.instAddCommMonoid` `ContrMod.instModuleReal` `inclCongrRealLorentz` `LorentzGroup` `lorentzGroupIsGroup` `Contr` `SL2C.toLorentzGroup`	—	`ContrℂModule.ext` `complexContrBasis_ρ_val` `inclCongrRealLorentz_val` `LorentzGroup.toComplex_mulVec_ofReal`

---

← Back to Index