Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `complexLorentzTensor`, `Color`, `complexLorentzTensorSyntax`, `instDecidableEqColor`, `instDecidableEqHomOverColorColorMkFin`, `instDecidableEqLeftColorMkFin`, `instFintypeLeftColorMkFin`, `«termℂT(_)»`»)	8
Theorems `FD_obj_down`, `FD_obj_up`, `basis_contr`, `basis_downL_eq`, `basis_downR_eq`, `basis_down_eq`, `basis_eq_complexCoBasisFin4`, `basis_eq_complexContrBasisFin4`, `basis_upL_eq`, `basis_upR_eq`, `basis_up_eq`, `repr_ρ_basis_vector_down`, `repr_ρ_basis_vector_down_of_eq`, `repr_ρ_basis_vector_up`, `repr_ρ_basis_vector_up_of_eq`	15
Total	23

(root)

Definitions

Name	Category	Theorems
`complexLorentzTensor` 📖	CompOp	160 math math: `realLorentzTensor.prodT_toComplex`, `complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection`, `complexLorentzTensor.rightMetric_eq_basis`, `realLorentzTensor.tau_colorToComplex`, `complexLorentzTensor.contrMetric_contr_coMetric`, `PauliMatrix.pauliCo_contr_pauliContr`, `complexLorentzTensor.coContrUnit_eq_basis`, `PauliMatrix.smul_pauliCoDown`, `realLorentzTensor.toComplex_evalP_basisVector`, `complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis`, `complexLorentzTensor.altLeftLeftUnit_eq_ofRat`, `complexLorentzTensor.altLeftMetric_contr_leftMetric`, `realLorentzTensor.complexify_prod`, `realLorentzTensor.complex_repDim_up`, `complexLorentzTensor.altLeftMetric_eq_basis`, `complexLorentzTensor.altRightMetric_eq_fromConstPair`, `complexLorentzTensor.altRightRightUnit_eq_fromConstPair`, `complexLorentzTensor.rightAltRightUnit_eq_fromPairT`, `realLorentzTensor.toComplex_injective`, `realLorentzTensor.contrT_toComplex`, `complexLorentzTensor.contrMetric_symm`, `complexLorentzTensor.altLeftMetric_antisymm`, `complexLorentzTensor.repr_ρ_basis_vector_up_of_eq`, `PauliMatrix.toTensor_smul_eq_self`, `PauliMatrix.pauliCoDown_eq_ofRat`, `complexLorentzTensor.basis_downR_eq`, `complexLorentzTensor.altLeftMetric_eq_fromPairT`, `complexLorentzTensor.altLeftMetric_eq_ofRat`, `complexLorentzTensor.rightAltRightUnit_eq_basis`, `complexLorentzTensor.leftMetric_contr_altLeftMetric`, `complexLorentzTensor.basis_up_eq`, `complexLorentzTensor.leftAltLeftUnit_eq_leftBasis_altLeftBasis`, `complexLorentzTensor.rightAltRightUnit_eq_rightBasis_altRightBasis`, `complexLorentzTensor.contrMetric_eq_complexContrBasisFin4`, `complexLorentzTensor.coMetric_symm`, `complexLorentzTensor.ofRat_basis_repr_apply`, `complexLorentzTensor.altRightMetric_eq_altRightBasis`, `complexLorentzTensor.altLeftLeftUnit_eq_basis`, `realLorentzTensor.ComponentIdx.complexify_apply`, `PauliMatrix.pauliCoDown_trace_pauliCo`, `complexLorentzTensor.basis_contr`, `realLorentzTensor.toComplex_pure_basisVector`, `complexLorentzTensor.actionT_altRightRightUnit`, `complexLorentzTensor.actionT_rightAltRightUnit`, `complexLorentzTensor.actionT_coContrUnit`, `complexLorentzTensor.actionT_altLeftLeftUnit`, `complexLorentzTensor.permT_ofRat`, `complexLorentzTensor.rightMetric_eq_rightBasis`, `complexLorentzTensor.contrMetric_eq_complexContrBasis`, `complexLorentzTensor.contrCoUnit_eq_fromConstPair`, `complexLorentzTensor.coContrUnit_eq_ofRat`, `complexLorentzTensor.actionT_rightMetric`, `complexLorentzTensor.basis_downL_eq`, `complexLorentzTensor.coMetric_contr_contrMetric`, `complexLorentzTensor.leftAltLeftUnit_eq_fromPairT`, `complexLorentzTensor.basis_upR_eq`, `complexLorentzTensor.leftMetric_eq_basis`, `PauliMatrix.smul_pauliCo`, `complexLorentzTensor.altRightMetric_eq_ofRat`, `complexLorentzTensor.coContrUnit_symm`, `complexLorentzTensor.contrMetric_eq_fromPairT`, `PauliMatrix.pauliContrDown_ofRat`, `complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4`, `complexLorentzTensor.basis_eq_complexContrBasisFin4`, `complexLorentzTensor.leftAltLeftUnit_eq_ofRat`, `complexLorentzTensor.altRightRightUnit_eq_ofRat`, `complexLorentzTensor.coMetric_eq_ofRat`, `complexLorentzTensor.leftMetric_eq_leftBasis`, `complexLorentzTensor.basis_eq_ofRat`, `complexLorentzTensor.altRightRightUnit_eq_fromPairT`, `realLorentzTensor.toComplex_eq_sum_basis`, `complexLorentzTensor.contrCoUnit_eq_ofRat`, `complexLorentzTensor.leftMetric_antisymm`, `complexLorentzTensor.actionT_contrMetric`, `complexLorentzTensor.altRightMetric_eq_basis`, `complexLorentzTensor.altLeftMetric_eq_fromConstPair`, `realLorentzTensor.permT_toComplex`, `complexLorentzTensor.coMetric_eq_basis`, `complexLorentzTensor.rightMetric_eq_ofRat`, `realLorentzTensor.evalT_toComplex`, `complexLorentzTensor.rightAltRightUnit_eq_ofRat`, `complexLorentzTensor.altRightMetric_eq_fromPairT`, `complexLorentzTensor.altRightRightUnit_eq_altRightBasis_rightBasis`, `complexLorentzTensor.contrT_ofRat`, `complexLorentzTensor.leftAltLeftUnit_eq_fromConstPair`, `complexLorentzTensor.basis_down_eq`, `complexLorentzTensor.actionT_leftMetric`, `realLorentzTensor.ComponentIdx.complexify_comp_dropPairEmb`, `complexLorentzTensor.contrCoUnit_symm`, `complexLorentzTensor.altRightMetric_contr_rightMetric`, `PauliMatrix.smul_pauliContrDown`, `complexLorentzTensor.rightMetric_eq_fromConstPair`, `realLorentzTensor.toComplex_equivariant`, `complexLorentzTensor.altLeftLeftUnit_eq_altLeftBasis_leftBasis`, `realLorentzTensor.toComplex_eq_zero_iff`, `complexLorentzTensor.actionT_coMetric`, `complexLorentzTensor.coContrUnit_eq_fromPairT`, `PauliMatrix.toTensor_symm_apply`, `complexLorentzTensor.rightAltRightUnit_eq_fromConstPair`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4`, `realLorentzTensor.toComplex_map_smul`, `realLorentzTensor.permT_basis_complex`, `complexLorentzTensor.actionT_leftAltLeftUnit`, `complexLorentzTensor.FD_obj_down`, `complexLorentzTensor.contrMetric_eq_basis`, `complexLorentzTensor.contrCoUnit_eq_basis`, `PauliMatrix.smul_eq_self`, `complexLorentzTensor.rightMetric_antisymm`, `PauliMatrix.toTensor_symm_basis`, `complexLorentzTensor.contrCoUnit_eq_fromPairT`, `complexLorentzTensor.altRightMetric_antisymm`, `complexLorentzTensor.leftMetric_eq_fromPairT`, `PauliMatrix.toTensor_basis_expand`, `complexLorentzTensor.rightMetric_eq_fromPairT`, `complexLorentzTensor.coMetric_eq_complexCoBasisFin4`, `complexLorentzTensor.leftMetric_eq_fromConstPair`, `complexLorentzTensor.altLeftMetric_eq_altLeftBasis`, `complexLorentzTensor.coMetric_eq_complexCoBasis`, `realLorentzTensor.complex_repDim_down`, `PauliMatrix.auliContrDown_pauliContr_mul_add`, `complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis`, `realLorentzTensor.toComplex_equivariant_slot_repr_up`, `complexLorentzTensor.basis_eq_complexCoBasisFin4`, `complexLorentzTensor.leftMetric_eq_ofRat`, `complexLorentzTensor.leftAltLeftUnit_eq_basis`, `complexLorentzTensor.actionT_altRightMetric`, `PauliMatrix.toTensor_eq_asConsTensor`, `complexLorentzTensor.repr_ρ_basis_vector_down`, `complexLorentzTensor.actionT_contrCoUnit`, `complexLorentzTensor.rightAltRightUnit_symm`, `complexLorentzTensor.contrMetric_eq_ofRat`, `realLorentzTensor.toComplex_basis`, `complexLorentzTensor.prodT_ofRat_ofRat`, `complexLorentzTensor.coMetric_eq_fromPairT`, `complexLorentzTensor.coContrUnit_eq_fromConstPair`, `PauliMatrix.toTensor_eq_ofRat`, `realLorentzTensor.toComplex_contrP_basisVector`, `PauliMatrix.pauliContr_mul_pauliContrDown_add`, `complexLorentzTensor.contr_basis_ratComplexNum`, `complexLorentzTensor.altLeftLeftUnit_eq_fromPairT`, `complexLorentzTensor.altLeftLeftUnit_symm`, `complexLorentzTensor.coMetric_eq_fromConstPair`, `complexLorentzTensor.leftAltLeftUnit_symm`, `complexLorentzTensor.altLeftLeftUnit_eq_fromConstPair`, `complexLorentzTensor.altRightRightUnit_eq_basis`, `realLorentzTensor.ComponentIdx.complexify_comp_succAbove`, `complexLorentzTensor.FD_obj_up`, `realLorentzTensor.ComponentIdx.complexify_toFun_apply`, `complexLorentzTensor.contrMetric_eq_fromConstPair`, `complexLorentzTensor.rightMetric_contr_altRightMetric`, `complexLorentzTensor.repr_ρ_basis_vector_up`, `complexLorentzTensor.basis_upL_eq`, `complexLorentzTensor.antiSymm_contr_symm`, `complexLorentzTensor.altRightRightUnit_symm`, `PauliMatrix.pauliCo_eq_ofRat`, `complexLorentzTensor.repr_ρ_basis_vector_down_of_eq`, `PauliMatrix.pauliCo_trace_pauliCoDown`, `complexLorentzTensor.actionT_altLeftMetric`, `realLorentzTensor.toComplex_repr`, `realLorentzTensor.toComplex_equivariant_slot_repr_down`

complexLorentzTensor

Definitions

Name	Category	Theorems
`Color` 📖	CompData	164 math math: `realLorentzTensor.prodT_toComplex`, `contrT_ofRat_eq_sum_dropPairSection`, `rightMetric_eq_basis`, `realLorentzTensor.tau_colorToComplex`, `contrMetric_contr_coMetric`, `PauliMatrix.pauliCo_contr_pauliContr`, `coContrUnit_eq_basis`, `PauliMatrix.smul_pauliCoDown`, `realLorentzTensor.toComplex_evalP_basisVector`, `coContrUnit_eq_complexCoBasis_complexContrBasis`, `altLeftLeftUnit_eq_ofRat`, `altLeftMetric_contr_leftMetric`, `realLorentzTensor.complexify_prod`, `realLorentzTensor.complex_repDim_up`, `altLeftMetric_eq_basis`, `altRightMetric_eq_fromConstPair`, `realLorentzTensor.colorToComplex_comp_eq_match`, `altRightRightUnit_eq_fromConstPair`, `rightAltRightUnit_eq_fromPairT`, `realLorentzTensor.toComplex_injective`, `realLorentzTensor.contrT_toComplex`, `contrMetric_symm`, `altLeftMetric_antisymm`, `repr_ρ_basis_vector_up_of_eq`, `PauliMatrix.toTensor_smul_eq_self`, `PauliMatrix.pauliCoDown_eq_ofRat`, `basis_downR_eq`, `altLeftMetric_eq_fromPairT`, `altLeftMetric_eq_ofRat`, `rightAltRightUnit_eq_basis`, `leftMetric_contr_altLeftMetric`, `basis_up_eq`, `leftAltLeftUnit_eq_leftBasis_altLeftBasis`, `rightAltRightUnit_eq_rightBasis_altRightBasis`, `contrMetric_eq_complexContrBasisFin4`, `coMetric_symm`, `ofRat_basis_repr_apply`, `altRightMetric_eq_altRightBasis`, `altLeftLeftUnit_eq_basis`, `realLorentzTensor.ComponentIdx.complexify_apply`, `PauliMatrix.pauliCoDown_trace_pauliCo`, `basis_contr`, `realLorentzTensor.toComplex_pure_basisVector`, `actionT_altRightRightUnit`, `actionT_rightAltRightUnit`, `actionT_coContrUnit`, `actionT_altLeftLeftUnit`, `permT_ofRat`, `rightMetric_eq_rightBasis`, `contrMetric_eq_complexContrBasis`, `contrCoUnit_eq_fromConstPair`, `coContrUnit_eq_ofRat`, `realLorentzTensor.permCond_prodTColorToComplex`, `actionT_rightMetric`, `realLorentzTensor.colorToComplex_append`, `basis_downL_eq`, `coMetric_contr_contrMetric`, `leftAltLeftUnit_eq_fromPairT`, `basis_upR_eq`, `leftMetric_eq_basis`, `PauliMatrix.smul_pauliCo`, `altRightMetric_eq_ofRat`, `coContrUnit_symm`, `contrMetric_eq_fromPairT`, `PauliMatrix.pauliContrDown_ofRat`, `coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4`, `basis_eq_complexContrBasisFin4`, `leftAltLeftUnit_eq_ofRat`, `altRightRightUnit_eq_ofRat`, `coMetric_eq_ofRat`, `leftMetric_eq_leftBasis`, `basis_eq_ofRat`, `altRightRightUnit_eq_fromPairT`, `realLorentzTensor.toComplex_eq_sum_basis`, `contrCoUnit_eq_ofRat`, `leftMetric_antisymm`, `actionT_contrMetric`, `altRightMetric_eq_basis`, `altLeftMetric_eq_fromConstPair`, `realLorentzTensor.permT_toComplex`, `coMetric_eq_basis`, `rightMetric_eq_ofRat`, `realLorentzTensor.evalT_toComplex`, `rightAltRightUnit_eq_ofRat`, `altRightMetric_eq_fromPairT`, `altRightRightUnit_eq_altRightBasis_rightBasis`, `contrT_ofRat`, `leftAltLeftUnit_eq_fromConstPair`, `basis_down_eq`, `actionT_leftMetric`, `realLorentzTensor.ComponentIdx.complexify_comp_dropPairEmb`, `contrCoUnit_symm`, `altRightMetric_contr_rightMetric`, `PauliMatrix.smul_pauliContrDown`, `rightMetric_eq_fromConstPair`, `realLorentzTensor.toComplex_equivariant`, `altLeftLeftUnit_eq_altLeftBasis_leftBasis`, `realLorentzTensor.toComplex_eq_zero_iff`, `actionT_coMetric`, `coContrUnit_eq_fromPairT`, `PauliMatrix.toTensor_symm_apply`, `rightAltRightUnit_eq_fromConstPair`, `contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4`, `realLorentzTensor.toComplex_map_smul`, `realLorentzTensor.permT_basis_complex`, `actionT_leftAltLeftUnit`, `FD_obj_down`, `contrMetric_eq_basis`, `contrCoUnit_eq_basis`, `PauliMatrix.smul_eq_self`, `rightMetric_antisymm`, `PauliMatrix.toTensor_symm_basis`, `contrCoUnit_eq_fromPairT`, `altRightMetric_antisymm`, `leftMetric_eq_fromPairT`, `PauliMatrix.toTensor_basis_expand`, `rightMetric_eq_fromPairT`, `coMetric_eq_complexCoBasisFin4`, `leftMetric_eq_fromConstPair`, `altLeftMetric_eq_altLeftBasis`, `coMetric_eq_complexCoBasis`, `realLorentzTensor.complex_repDim_down`, `PauliMatrix.auliContrDown_pauliContr_mul_add`, `contrCoUnit_eq_complexContrBasis_complexCoBasis`, `realLorentzTensor.toComplex_equivariant_slot_repr_up`, `basis_eq_complexCoBasisFin4`, `leftMetric_eq_ofRat`, `leftAltLeftUnit_eq_basis`, `actionT_altRightMetric`, `PauliMatrix.toTensor_eq_asConsTensor`, `repr_ρ_basis_vector_down`, `actionT_contrCoUnit`, `rightAltRightUnit_symm`, `contrMetric_eq_ofRat`, `realLorentzTensor.toComplex_basis`, `prodT_ofRat_ofRat`, `coMetric_eq_fromPairT`, `coContrUnit_eq_fromConstPair`, `PauliMatrix.toTensor_eq_ofRat`, `realLorentzTensor.toComplex_contrP_basisVector`, `PauliMatrix.pauliContr_mul_pauliContrDown_add`, `contr_basis_ratComplexNum`, `altLeftLeftUnit_eq_fromPairT`, `altLeftLeftUnit_symm`, `coMetric_eq_fromConstPair`, `leftAltLeftUnit_symm`, `altLeftLeftUnit_eq_fromConstPair`, `altRightRightUnit_eq_basis`, `realLorentzTensor.ComponentIdx.complexify_comp_succAbove`, `FD_obj_up`, `realLorentzTensor.permCond_colorToComplex`, `realLorentzTensor.ComponentIdx.complexify_toFun_apply`, `contrMetric_eq_fromConstPair`, `rightMetric_contr_altRightMetric`, `repr_ρ_basis_vector_up`, `basis_upL_eq`, `antiSymm_contr_symm`, `altRightRightUnit_symm`, `PauliMatrix.pauliCo_eq_ofRat`, `repr_ρ_basis_vector_down_of_eq`, `PauliMatrix.pauliCo_trace_pauliCoDown`, `actionT_altLeftMetric`, `realLorentzTensor.toComplex_repr`, `realLorentzTensor.toComplex_equivariant_slot_repr_down`
`complexLorentzTensorSyntax` 📖	CompOp	—
`instDecidableEqColor` 📖	CompOp	—
`instDecidableEqHomOverColorColorMkFin` 📖	CompOp	—
`instDecidableEqLeftColorMkFin` 📖	CompOp	—
`instFintypeLeftColorMkFin` 📖	CompOp	—
`«termℂT(_)»` 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FD_obj_down` 📖	mathematical	—	`Color` `TensorSpecies.FD` `complexLorentzTensor` `Color.down` `Lorentz.complexCo`	—	—
`FD_obj_up` 📖	mathematical	—	`Color` `TensorSpecies.FD` `complexLorentzTensor` `Color.up` `Lorentz.complexContr`	—	—
`basis_contr` 📖	mathematical	—	`TensorSpecies.castToField` `Color` `complexLorentzTensor` `IndexNotation.OverColor.Discrete.pairτ` `TensorSpecies.FD` `TensorSpecies.τ` `TensorSpecies.contr` `TensorSpecies.repDim` `TensorSpecies.basis`	—	`Fermion.leftAltContraction_basis` `Fermion.altLeftContraction_basis` `Fermion.rightAltContraction_basis` `Fermion.altRightContraction_basis` `Lorentz.contrCoContraction_basis` `Lorentz.coContrContraction_basis`
`basis_downL_eq` 📖	mathematical	—	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `Color.downL` `TensorSpecies.FD` `TensorSpecies.basis` `Fermion.altLeftHanded` `Fermion.altLeftBasis`	—	—
`basis_downR_eq` 📖	mathematical	—	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `Color.downR` `TensorSpecies.FD` `TensorSpecies.basis` `Fermion.altRightHanded` `Fermion.altRightBasis`	—	—
`basis_down_eq` 📖	mathematical	—	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `Color.down` `TensorSpecies.FD` `TensorSpecies.basis` `Lorentz.complexCo` `Lorentz.complexCoBasisFin4`	—	—
`basis_eq_complexCoBasisFin4` 📖	mathematical	—	`TensorSpecies.basis` `Color` `complexLorentzTensor` `Color.down` `Lorentz.complexCoBasisFin4`	—	`basis_down_eq`
`basis_eq_complexContrBasisFin4` 📖	mathematical	—	`TensorSpecies.basis` `Color` `complexLorentzTensor` `Color.up` `Lorentz.complexContrBasisFin4`	—	`basis_up_eq`
`basis_upL_eq` 📖	mathematical	—	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `Color.upL` `TensorSpecies.FD` `TensorSpecies.basis` `Fermion.leftHanded` `Fermion.leftBasis`	—	—
`basis_upR_eq` 📖	mathematical	—	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `Color.upR` `TensorSpecies.FD` `TensorSpecies.basis` `Fermion.rightHanded` `Fermion.rightBasis`	—	—
`basis_up_eq` 📖	mathematical	—	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `Color.up` `TensorSpecies.FD` `TensorSpecies.basis` `Lorentz.complexContr` `Lorentz.complexContrBasisFin4`	—	—
`repr_ρ_basis_vector_down` 📖	mathematical	—	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `Color.down` `TensorSpecies.FD` `TensorSpecies.basis` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `Lorentz.SL2C.toLorentzGroup`	—	`Lorentz.complexCoBasis_reindex_apply_eq_fin4` `basis_eq_complexCoBasisFin4` `Lorentz.complexCoBasis_ρ_apply`
`repr_ρ_basis_vector_down_of_eq` 📖	mathematical	`Color.down`	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `TensorSpecies.FD` `TensorSpecies.basis` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `Lorentz.SL2C.toLorentzGroup`	—	`basis_eq_complexCoBasisFin4` `repr_ρ_basis_vector_down`
`repr_ρ_basis_vector_up` 📖	mathematical	—	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `Color.up` `TensorSpecies.FD` `TensorSpecies.basis` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `Lorentz.SL2C.toLorentzGroup`	—	`Lorentz.complexContrBasis_reindex_apply_eq_fin4` `basis_eq_complexContrBasisFin4` `Lorentz.complexContrBasis_ρ_apply`
`repr_ρ_basis_vector_up_of_eq` 📖	mathematical	`Color.up`	`TensorSpecies.repDim` `Color` `complexLorentzTensor` `TensorSpecies.FD` `TensorSpecies.basis` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.toComplex` `Lorentz.SL2C.toLorentzGroup`	—	`basis_eq_complexContrBasisFin4` `repr_ρ_basis_vector_up`

---

← Back to Index