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, complexCoBasisFin4_eq_reindex, complexCoBasis_reindex_apply_eq_fin4, complexCoBasis_toFin13ℂ, complexCoBasis_ρ_apply, complexContrBasisFin4_apply_one, complexContrBasisFin4_apply_succ, complexContrBasisFin4_apply_three, complexContrBasisFin4_apply_two, complexContrBasisFin4_apply_zero, complexContrBasisFin4_eq_reindex, complexContrBasis_of_real, complexContrBasis_reindex_apply_eq_fin4, complexContrBasis_toFin13ℂ, complexContrBasis_ρ_apply, complexContrBasis_ρ_val, inclCongrRealLorentz_val, inclCongrRealLorentz_ρ	22
Total	29

Lorentz

Definitions

Name	Category	Theorems
complexCo 📖	CompOp	45 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', complexCoBasisFin4_eq_reindex, 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.FD_obj_down, complexLorentzTensor.coMetric_eq_complexCoBasisFin4, coContrUnitVal_expand_tmul, contrCoToMatrix_ρ, complexLorentzTensor.coMetric_eq_complexCoBasis, complexCoBasisFin4_apply_two, complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis, coContrToMatrix_ρ_symm, complexCoBasis_reindex_apply_eq_fin4, 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	19 math math: complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis, complexCoBasisFin4_apply_one, coCoToMatrix_symm_expand_tmul, contrCoUnitVal_expand_tmul, contrCoContraction_basis', complexCoBasisFin4_eq_reindex, 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, complexCoBasis_reindex_apply_eq_fin4, coMetricVal_expand_tmul, contrCoToMatrix_symm_expand_tmul, complexCoBasisFin4_apply_zero
complexCoBasisFin4 📖	CompOp	13 math math: contrCoContraction_basis, complexCoBasisFin4_apply_one, complexCoBasisFin4_eq_reindex, 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, complexLorentzTensor.basis_eq_complexCoBasisFin4, complexCoBasis_reindex_apply_eq_fin4, complexCoBasisFin4_apply_zero
complexContr 📖	CompOp	54 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_eq_reindex, 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, complexContrBasis_reindex_apply_eq_fin4, coContrToMatrix_ρ_symm, complexContrBasis_of_real, complexLorentzTensor.FD_obj_up, contrCoContraction_apply_metric, contrCoUnit_apply_one, coContrUnit_apply_one, coContrContraction_tmul_symm, contrContrToMatrix_ρ, contr_contrCoUnit, contrCoToMatrix_symm_expand_tmul, complexContrBasisFin4_apply_two
complexContrBasis 📖	CompOp	24 math math: complexContrBasis_toFin13ℂ, complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis, contrContrToMatrix_symm_expand_tmul, complexContrBasis_ρ_apply, complexContrBasisFin4_eq_reindex, 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_reindex_apply_eq_fin4, complexContrBasis_of_real, contrCoToMatrix_symm_expand_tmul, complexContrBasisFin4_apply_two
complexContrBasisFin4 📖	CompOp	14 math math: contrCoContraction_basis, complexContrBasisFin4_eq_reindex, complexContrBasisFin4_apply_three, complexLorentzTensor.basis_up_eq, complexLorentzTensor.contrMetric_eq_complexContrBasisFin4, complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4, complexLorentzTensor.basis_eq_complexContrBasisFin4, complexContrBasisFin4_apply_succ, complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4, coContrContraction_basis, complexContrBasisFin4_apply_one, complexContrBasisFin4_apply_zero, complexContrBasis_reindex_apply_eq_fin4, 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	—	—
complexCoBasisFin4_eq_reindex 📖	mathematical	—	complexCoBasisFin4 complexCo complexCoBasis	—	—
complexCoBasis_reindex_apply_eq_fin4 📖	mathematical	—	complexCo complexCoBasis complexCoBasisFin4	—	—
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	—	—
complexContrBasisFin4_eq_reindex 📖	mathematical	—	complexContrBasisFin4 complexContr 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_reindex_apply_eq_fin4 📖	mathematical	—	complexContr complexContrBasis complexContrBasisFin4	—	—
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