Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `altLeftBasis`, `altLeftHanded`, `altRightBasis`, `altRightHanded`, `leftBasis`, `leftHanded`, `leftHandedAltEquiv`, `leftHandedAltTo`, `leftHandedToAlt`, `rightBasis`, `rightHanded`, `rightHandedWeylAltEquiv`, `rightHandedWeylAltEquiv_equivariant`	13
Theorems `altLeftBasis_toFin2ℂ`, `altLeftBasis_ρ_apply`, `altRightBasis_toFin2ℂ`, `altRightBasis_ρ_apply`, `leftBasis_toFin2ℂ`, `leftBasis_ρ_apply`, `leftHandedAltEquiv_hom_hom_apply`, `leftHandedAltEquiv_inv_hom_apply`, `leftHandedAltTo_hom_apply`, `leftHandedToAlt_hom_apply`, `rightBasis_toFin2ℂ`, `rightBasis_ρ_apply`	12
Total	25

Fermion

Definitions

Name	Category	Theorems
`altLeftBasis` 📖	CompOp	15 math math: `altLeftBasis_ρ_apply`, `altLeftContraction_basis`, `leftAltContraction_basis`, `complexLorentzTensor.leftAltLeftUnit_eq_leftBasis_altLeftBasis`, `altLeftMetricVal_expand_tmul`, `altLeftBasis_toFin2ℂ`, `altLeftLeftUnitVal_expand_tmul`, `complexLorentzTensor.basis_downL_eq`, `leftAltLeftToMatrix_symm_expand_tmul`, `altLeftaltLeftToMatrix_symm_expand_tmul`, `complexLorentzTensor.altLeftLeftUnit_eq_altLeftBasis_leftBasis`, `leftAltLeftUnitVal_expand_tmul`, `complexLorentzTensor.altLeftMetric_eq_altLeftBasis`, `altLeftLeftToMatrix_symm_expand_tmul`, `altLeftAltRightToMatrix_symm_expand_tmul`
`altLeftHanded` 📖	CompOp	41 math math: `altLeftMetric_apply_one`, `altLeftBasis_ρ_apply`, `altLeftLeftUnit_apply_one`, `altLeftContraction_basis`, `altLeftLeftToMatrix_ρ`, `leftAltContraction_tmul_symm`, `altLeftAltRightToMatrix_ρ`, `leftAltContraction_basis`, `altLeftAltRightToMatrix_ρ_symm`, `complexLorentzTensor.leftAltLeftUnit_eq_leftBasis_altLeftBasis`, `contr_altLeftLeftUnit`, `altLeftMetricVal_expand_tmul`, `altLeftBasis_toFin2ℂ`, `altLeftContraction_hom_tmul`, `altLeftLeftUnitVal_expand_tmul`, `complexLorentzTensor.basis_downL_eq`, `altLeftaltLeftToMatrix_ρ`, `leftAltLeftUnit_apply_one`, `leftAltLeftToMatrix_symm_expand_tmul`, `altLeftAltRightToMatrix_ρ_symm_selfAdjoint`, `contr_leftAltLeftUnit`, `leftHandedAltEquiv_hom_hom_apply`, `altLeftContraction_apply_metric`, `altLeftaltLeftToMatrix_symm_expand_tmul`, `altLeftLeftToMatrix_ρ_symm`, `complexLorentzTensor.altLeftLeftUnit_eq_altLeftBasis_leftBasis`, `leftHandedAltEquiv_inv_hom_apply`, `leftAltLeftUnitVal_expand_tmul`, `altLeftContraction_tmul_symm`, `leftAltLeftToMatrix_ρ`, `leftAltLeftUnit_symm`, `complexLorentzTensor.altLeftMetric_eq_altLeftBasis`, `leftAltContraction_apply_metric`, `leftAltLeftToMatrix_ρ_symm`, `altLeftLeftUnit_symm`, `altLeftLeftToMatrix_symm_expand_tmul`, `altLeftaltLeftToMatrix_ρ_symm`, `leftAltContraction_hom_tmul`, `leftHandedToAlt_hom_apply`, `leftHandedAltTo_hom_apply`, `altLeftAltRightToMatrix_symm_expand_tmul`
`altRightBasis` 📖	CompOp	15 math math: `rightAltContraction_basis`, `complexLorentzTensor.basis_downR_eq`, `altRightMetricVal_expand_tmul`, `complexLorentzTensor.rightAltRightUnit_eq_rightBasis_altRightBasis`, `complexLorentzTensor.altRightMetric_eq_altRightBasis`, `altRightAltRightToMatrix_symm_expand_tmul`, `rightAltRightToMatrix_symm_expand_tmul`, `altRightBasis_ρ_apply`, `complexLorentzTensor.altRightRightUnit_eq_altRightBasis_rightBasis`, `altRightBasis_toFin2ℂ`, `rightAltRightUnitVal_expand_tmul`, `altRightContraction_basis`, `altRightRightToMatrix_symm_expand_tmul`, `altLeftAltRightToMatrix_symm_expand_tmul`, `altRightRightUnitVal_expand_tmul`
`altRightHanded` 📖	CompOp	37 math math: `rightAltContraction_basis`, `contr_altRightRightUnit`, `altRightRightUnit_symm`, `complexLorentzTensor.basis_downR_eq`, `altRightMetricVal_expand_tmul`, `altLeftAltRightToMatrix_ρ`, `rightAltContraction_hom_tmul`, `altLeftAltRightToMatrix_ρ_symm`, `complexLorentzTensor.rightAltRightUnit_eq_rightBasis_altRightBasis`, `complexLorentzTensor.altRightMetric_eq_altRightBasis`, `altRightAltRightToMatrix_symm_expand_tmul`, `rightAltRightToMatrix_symm_expand_tmul`, `altRightMetric_apply_one`, `rightAltContraction_apply_metric`, `altRightAltRightToMatrix_ρ`, `altRightRightToMatrix_ρ`, `altLeftAltRightToMatrix_ρ_symm_selfAdjoint`, `altRightBasis_ρ_apply`, `altRightAltRightToMatrix_ρ_symm`, `complexLorentzTensor.altRightRightUnit_eq_altRightBasis_rightBasis`, `rightAltRightToMatrix_ρ`, `altRightBasis_toFin2ℂ`, `altRightContraction_hom_tmul`, `rightAltRightUnit_symm`, `contr_rightAltRightUnit`, `rightAltRightUnitVal_expand_tmul`, `rightAltRightUnit_apply_one`, `rightAltRightToMatrix_ρ_symm`, `altRightContraction_basis`, `altRightRightToMatrix_ρ_symm`, `altRightContraction_tmul_symm`, `rightAltContraction_tmul_symm`, `altRightContraction_apply_metric`, `altRightRightToMatrix_symm_expand_tmul`, `altRightRightUnit_apply_one`, `altLeftAltRightToMatrix_symm_expand_tmul`, `altRightRightUnitVal_expand_tmul`
`leftBasis` 📖	CompOp	20 math math: `altLeftContraction_basis`, `leftLeftToMatrix_symm_expand_tmul`, `leftAltContraction_basis`, `leftBasis_ρ_apply`, `complexLorentzTensor.leftAltLeftUnit_eq_leftBasis_altLeftBasis`, `altLeftLeftUnitVal_expand_tmul`, `leftAltLeftToMatrix_symm_expand_tmul`, `leftMetricVal_expand_tmul`, `complexLorentzTensor.leftMetric_eq_leftBasis`, `PauliMatrix.asTensor_expand`, `complexLorentzTensor.altLeftLeftUnit_eq_altLeftBasis_leftBasis`, `leftAltLeftUnitVal_expand_tmul`, `PauliMatrix.leftRightToMatrix_σSA_inl_0_expand`, `PauliMatrix.leftRightToMatrix_σSA_inr_1_expand`, `leftRightToMatrix_symm_expand_tmul`, `altLeftLeftToMatrix_symm_expand_tmul`, `PauliMatrix.leftRightToMatrix_σSA_inr_0_expand`, `complexLorentzTensor.basis_upL_eq`, `leftBasis_toFin2ℂ`, `PauliMatrix.leftRightToMatrix_σSA_inr_2_expand`
`leftHanded` 📖	CompOp	48 math math: `altLeftLeftUnit_apply_one`, `altLeftContraction_basis`, `leftMetric_apply_one`, `leftLeftToMatrix_symm_expand_tmul`, `altLeftLeftToMatrix_ρ`, `leftAltContraction_tmul_symm`, `leftLeftToMatrix_ρ`, `leftAltContraction_basis`, `leftBasis_ρ_apply`, `complexLorentzTensor.leftAltLeftUnit_eq_leftBasis_altLeftBasis`, `contr_altLeftLeftUnit`, `altLeftContraction_hom_tmul`, `altLeftLeftUnitVal_expand_tmul`, `leftAltLeftUnit_apply_one`, `leftAltLeftToMatrix_symm_expand_tmul`, `leftMetricVal_expand_tmul`, `complexLorentzTensor.leftMetric_eq_leftBasis`, `PauliMatrix.asConsTensor_apply_one`, `PauliMatrix.asTensor_expand`, `leftLeftToMatrix_ρ_symm`, `contr_leftAltLeftUnit`, `leftHandedAltEquiv_hom_hom_apply`, `altLeftContraction_apply_metric`, `altLeftLeftToMatrix_ρ_symm`, `complexLorentzTensor.altLeftLeftUnit_eq_altLeftBasis_leftBasis`, `leftRightToMatrix_ρ_symm`, `leftHandedAltEquiv_inv_hom_apply`, `leftAltLeftUnitVal_expand_tmul`, `PauliMatrix.leftRightToMatrix_σSA_inl_0_expand`, `altLeftContraction_tmul_symm`, `leftRightToMatrix_ρ_symm_selfAdjoint`, `leftAltLeftToMatrix_ρ`, `PauliMatrix.leftRightToMatrix_σSA_inr_1_expand`, `leftAltLeftUnit_symm`, `leftAltContraction_apply_metric`, `PauliMatrix.asTensor_expand_complexContrBasis`, `leftRightToMatrix_symm_expand_tmul`, `leftAltLeftToMatrix_ρ_symm`, `altLeftLeftUnit_symm`, `altLeftLeftToMatrix_symm_expand_tmul`, `PauliMatrix.leftRightToMatrix_σSA_inr_0_expand`, `leftAltContraction_hom_tmul`, `leftRightToMatrix_ρ`, `complexLorentzTensor.basis_upL_eq`, `leftHandedToAlt_hom_apply`, `leftHandedAltTo_hom_apply`, `leftBasis_toFin2ℂ`, `PauliMatrix.leftRightToMatrix_σSA_inr_2_expand`
`leftHandedAltEquiv` 📖	CompOp	2 math math: `leftHandedAltEquiv_hom_hom_apply`, `leftHandedAltEquiv_inv_hom_apply`
`leftHandedAltTo` 📖	CompOp	1 math math: `leftHandedAltTo_hom_apply`
`leftHandedToAlt` 📖	CompOp	1 math math: `leftHandedToAlt_hom_apply`
`rightBasis` 📖	CompOp	20 math math: `rightAltContraction_basis`, `complexLorentzTensor.rightAltRightUnit_eq_rightBasis_altRightBasis`, `rightAltRightToMatrix_symm_expand_tmul`, `complexLorentzTensor.rightMetric_eq_rightBasis`, `complexLorentzTensor.basis_upR_eq`, `PauliMatrix.asTensor_expand`, `rightMetricVal_expand_tmul`, `complexLorentzTensor.altRightRightUnit_eq_altRightBasis_rightBasis`, `rightBasis_ρ_apply`, `PauliMatrix.leftRightToMatrix_σSA_inl_0_expand`, `rightAltRightUnitVal_expand_tmul`, `PauliMatrix.leftRightToMatrix_σSA_inr_1_expand`, `altRightContraction_basis`, `leftRightToMatrix_symm_expand_tmul`, `PauliMatrix.leftRightToMatrix_σSA_inr_0_expand`, `altRightRightToMatrix_symm_expand_tmul`, `rightRightToMatrix_symm_expand_tmul`, `rightBasis_toFin2ℂ`, `altRightRightUnitVal_expand_tmul`, `PauliMatrix.leftRightToMatrix_σSA_inr_2_expand`
`rightHanded` 📖	CompOp	44 math math: `rightAltContraction_basis`, `contr_altRightRightUnit`, `altRightRightUnit_symm`, `rightAltContraction_hom_tmul`, `complexLorentzTensor.rightAltRightUnit_eq_rightBasis_altRightBasis`, `rightAltRightToMatrix_symm_expand_tmul`, `complexLorentzTensor.rightMetric_eq_rightBasis`, `rightAltContraction_apply_metric`, `complexLorentzTensor.basis_upR_eq`, `rightRightToMatrix_ρ`, `altRightRightToMatrix_ρ`, `PauliMatrix.asConsTensor_apply_one`, `PauliMatrix.asTensor_expand`, `rightMetricVal_expand_tmul`, `complexLorentzTensor.altRightRightUnit_eq_altRightBasis_rightBasis`, `rightAltRightToMatrix_ρ`, `altRightContraction_hom_tmul`, `rightRightToMatrix_ρ_symm`, `leftRightToMatrix_ρ_symm`, `rightAltRightUnit_symm`, `rightBasis_ρ_apply`, `PauliMatrix.leftRightToMatrix_σSA_inl_0_expand`, `leftRightToMatrix_ρ_symm_selfAdjoint`, `contr_rightAltRightUnit`, `rightAltRightUnitVal_expand_tmul`, `rightAltRightUnit_apply_one`, `rightAltRightToMatrix_ρ_symm`, `PauliMatrix.leftRightToMatrix_σSA_inr_1_expand`, `altRightContraction_basis`, `altRightRightToMatrix_ρ_symm`, `PauliMatrix.asTensor_expand_complexContrBasis`, `altRightContraction_tmul_symm`, `rightAltContraction_tmul_symm`, `leftRightToMatrix_symm_expand_tmul`, `altRightContraction_apply_metric`, `PauliMatrix.leftRightToMatrix_σSA_inr_0_expand`, `altRightRightToMatrix_symm_expand_tmul`, `rightRightToMatrix_symm_expand_tmul`, `rightBasis_toFin2ℂ`, `altRightRightUnit_apply_one`, `leftRightToMatrix_ρ`, `rightMetric_apply_one`, `altRightRightUnitVal_expand_tmul`, `PauliMatrix.leftRightToMatrix_σSA_inr_2_expand`
`rightHandedWeylAltEquiv` 📖	CompOp	—
`rightHandedWeylAltEquiv_equivariant` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`altLeftBasis_toFin2ℂ` 📖	mathematical	—	`AltLeftHandedModule.toFin2ℂ` `altLeftHanded` `altLeftBasis`	—	—
`altLeftBasis_ρ_apply` 📖	mathematical	—	`altLeftHanded` `altLeftBasis`	—	—
`altRightBasis_toFin2ℂ` 📖	mathematical	—	`AltRightHandedModule.toFin2ℂ` `altRightHanded` `altRightBasis`	—	—
`altRightBasis_ρ_apply` 📖	mathematical	—	`altRightHanded` `altRightBasis`	—	—
`leftBasis_toFin2ℂ` 📖	mathematical	—	`LeftHandedModule.toFin2ℂ` `leftHanded` `leftBasis`	—	—
`leftBasis_ρ_apply` 📖	mathematical	—	`leftHanded` `leftBasis`	—	—
`leftHandedAltEquiv_hom_hom_apply` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftHandedAltEquiv` `AltLeftHandedModule` `AltLeftHandedModule.instAddCommMonoid` `AltLeftHandedModule.instModuleComplex` `AltLeftHandedModule.toFin2ℂEquiv` `LeftHandedModule.toFin2ℂ`	—	—
`leftHandedAltEquiv_inv_hom_apply` 📖	mathematical	—	`altLeftHanded` `leftHanded` `leftHandedAltEquiv` `LeftHandedModule` `LeftHandedModule.instAddCommMonoid` `LeftHandedModule.instModuleComplex` `LeftHandedModule.toFin2ℂEquiv` `AltLeftHandedModule.toFin2ℂ`	—	—
`leftHandedAltTo_hom_apply` 📖	mathematical	—	`altLeftHanded` `leftHanded` `leftHandedAltTo` `LeftHandedModule` `LeftHandedModule.instAddCommMonoid` `LeftHandedModule.instModuleComplex` `LeftHandedModule.toFin2ℂEquiv` `AltLeftHandedModule.toFin2ℂ`	—	—
`leftHandedToAlt_hom_apply` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftHandedToAlt` `AltLeftHandedModule` `AltLeftHandedModule.instAddCommMonoid` `AltLeftHandedModule.instModuleComplex` `AltLeftHandedModule.toFin2ℂEquiv` `LeftHandedModule.toFin2ℂ`	—	—
`rightBasis_toFin2ℂ` 📖	mathematical	—	`RightHandedModule.toFin2ℂ` `rightHanded` `rightBasis`	—	—
`rightBasis_ρ_apply` 📖	mathematical	—	`rightHanded` `rightBasis`	—	—

---

← Back to Index