Basic

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

Statistics

Metric	Count
Definitions altLeftLeftUnit, altRightRightUnit, coContrUnit, contrCoUnit, leftAltLeftUnit, rightAltRightUnit, termδ, termδ', termδL, termδL', termδR, termδR'	12
Theorems actionT_altLeftLeftUnit, actionT_altRightRightUnit, actionT_coContrUnit, actionT_contrCoUnit, actionT_leftAltLeftUnit, actionT_rightAltRightUnit, altLeftLeftUnit_eq_altLeftBasis_leftBasis, altLeftLeftUnit_eq_basis, altLeftLeftUnit_eq_fromConstPair, altLeftLeftUnit_eq_fromPairT, altLeftLeftUnit_eq_ofRat, altRightRightUnit_eq_altRightBasis_rightBasis, altRightRightUnit_eq_basis, altRightRightUnit_eq_fromConstPair, altRightRightUnit_eq_fromPairT, altRightRightUnit_eq_ofRat, coContrUnit_eq_basis, coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4, coContrUnit_eq_complexCoBasis_complexContrBasis, coContrUnit_eq_fromConstPair, coContrUnit_eq_fromPairT, coContrUnit_eq_ofRat, contrCoUnit_eq_basis, contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4, contrCoUnit_eq_complexContrBasis_complexCoBasis, contrCoUnit_eq_fromConstPair, contrCoUnit_eq_fromPairT, contrCoUnit_eq_ofRat, leftAltLeftUnit_eq_basis, leftAltLeftUnit_eq_fromConstPair, leftAltLeftUnit_eq_fromPairT, leftAltLeftUnit_eq_leftBasis_altLeftBasis, leftAltLeftUnit_eq_ofRat, rightAltRightUnit_eq_basis, rightAltRightUnit_eq_fromConstPair, rightAltRightUnit_eq_fromPairT, rightAltRightUnit_eq_ofRat, rightAltRightUnit_eq_rightBasis_altRightBasis	38
Total	50

complexLorentzTensor

Definitions

Name	Category	Theorems
altLeftLeftUnit 📖	CompOp	9 math math: altLeftLeftUnit_eq_ofRat, altLeftMetric_contr_leftMetric, altLeftLeftUnit_eq_basis, actionT_altLeftLeftUnit, altLeftLeftUnit_eq_altLeftBasis_leftBasis, altLeftLeftUnit_eq_fromPairT, altLeftLeftUnit_symm, leftAltLeftUnit_symm, altLeftLeftUnit_eq_fromConstPair
altRightRightUnit 📖	CompOp	10 math math: altRightRightUnit_eq_fromConstPair, actionT_altRightRightUnit, altRightRightUnit_eq_ofRat, altRightRightUnit_eq_fromPairT, altRightRightUnit_eq_altRightBasis_rightBasis, altRightMetric_contr_rightMetric, PauliMatrix.auliContrDown_pauliContr_mul_add, rightAltRightUnit_symm, altRightRightUnit_eq_basis, altRightRightUnit_symm
coContrUnit 📖	CompOp	10 math math: coContrUnit_eq_basis, coContrUnit_eq_complexCoBasis_complexContrBasis, actionT_coContrUnit, coContrUnit_eq_ofRat, coMetric_contr_contrMetric, coContrUnit_symm, coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4, contrCoUnit_symm, coContrUnit_eq_fromPairT, coContrUnit_eq_fromConstPair
contrCoUnit 📖	CompOp	10 math math: contrMetric_contr_coMetric, contrCoUnit_eq_fromConstPair, coContrUnit_symm, contrCoUnit_eq_ofRat, contrCoUnit_symm, contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4, contrCoUnit_eq_basis, contrCoUnit_eq_fromPairT, contrCoUnit_eq_complexContrBasis_complexCoBasis, actionT_contrCoUnit
leftAltLeftUnit 📖	CompOp	10 math math: leftMetric_contr_altLeftMetric, leftAltLeftUnit_eq_leftBasis_altLeftBasis, leftAltLeftUnit_eq_fromPairT, leftAltLeftUnit_eq_ofRat, leftAltLeftUnit_eq_fromConstPair, actionT_leftAltLeftUnit, leftAltLeftUnit_eq_basis, PauliMatrix.pauliContr_mul_pauliContrDown_add, altLeftLeftUnit_symm, leftAltLeftUnit_symm
rightAltRightUnit 📖	CompOp	9 math math: rightAltRightUnit_eq_fromPairT, rightAltRightUnit_eq_basis, rightAltRightUnit_eq_rightBasis_altRightBasis, actionT_rightAltRightUnit, rightAltRightUnit_eq_ofRat, rightAltRightUnit_eq_fromConstPair, rightAltRightUnit_symm, rightMetric_contr_altRightMetric, altRightRightUnit_symm
termδ 📖	CompOp	—
termδ' 📖	CompOp	—
termδL 📖	CompOp	—
termδL' 📖	CompOp	—
termδR 📖	CompOp	—
termδR' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
actionT_altLeftLeftUnit 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downL Color.upL TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self altLeftLeftUnit	—	TensorSpecies.unitTensor_invariant
actionT_altRightRightUnit 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downR Color.upR TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self altRightRightUnit	—	TensorSpecies.unitTensor_invariant
actionT_coContrUnit 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.down Color.up TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self coContrUnit	—	TensorSpecies.unitTensor_invariant
actionT_contrCoUnit 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.up Color.down TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self contrCoUnit	—	TensorSpecies.unitTensor_invariant
actionT_leftAltLeftUnit 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upL Color.downL TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self leftAltLeftUnit	—	TensorSpecies.unitTensor_invariant
actionT_rightAltRightUnit 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upR Color.downR TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self rightAltRightUnit	—	TensorSpecies.unitTensor_invariant
altLeftLeftUnit_eq_altLeftBasis_leftBasis 📖	mathematical	—	altLeftLeftUnit TensorSpecies.Tensor Color complexLorentzTensor Color.downL Color.upL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Fermion.altLeftHanded Fermion.altLeftBasis Fermion.leftHanded Fermion.leftBasis	—	altLeftLeftUnit_eq_fromPairT Fermion.altLeftLeftUnitVal_expand_tmul
altLeftLeftUnit_eq_basis 📖	mathematical	—	altLeftLeftUnit TensorSpecies.repDim Color complexLorentzTensor Color.downL Color.upL TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis	—	altLeftLeftUnit_eq_altLeftBasis_leftBasis TensorSpecies.Tensor.fromPairT_apply_basis_repr
altLeftLeftUnit_eq_fromConstPair 📖	mathematical	—	altLeftLeftUnit TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.downL Color.upL Fermion.altLeftLeftUnit	—	Fermion.altLeftLeftUnit.eq_1
altLeftLeftUnit_eq_fromPairT 📖	mathematical	—	altLeftLeftUnit Color TensorSpecies.FD complexLorentzTensor Color.downL Color.upL TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Fermion.altLeftLeftUnitVal	—	altLeftLeftUnit_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Fermion.altLeftLeftUnit_apply_one
altLeftLeftUnit_eq_ofRat 📖	mathematical	—	altLeftLeftUnit PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.downL Color.upL TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim	—	altLeftLeftUnit_eq_basis basis_eq_ofRat
altRightRightUnit_eq_altRightBasis_rightBasis 📖	mathematical	—	altRightRightUnit TensorSpecies.Tensor Color complexLorentzTensor Color.downR Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Fermion.altRightHanded Fermion.altRightBasis Fermion.rightHanded Fermion.rightBasis	—	altRightRightUnit_eq_fromPairT Fermion.altRightRightUnitVal_expand_tmul
altRightRightUnit_eq_basis 📖	mathematical	—	altRightRightUnit TensorSpecies.repDim Color complexLorentzTensor Color.downR Color.upR TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis	—	altRightRightUnit_eq_altRightBasis_rightBasis TensorSpecies.Tensor.fromPairT_apply_basis_repr
altRightRightUnit_eq_fromConstPair 📖	mathematical	—	altRightRightUnit TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.downR Color.upR Fermion.altRightRightUnit	—	Fermion.altRightRightUnit.eq_1
altRightRightUnit_eq_fromPairT 📖	mathematical	—	altRightRightUnit Color TensorSpecies.FD complexLorentzTensor Color.downR Color.upR TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Fermion.altRightRightUnitVal	—	altRightRightUnit_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Fermion.altRightRightUnit_apply_one
altRightRightUnit_eq_ofRat 📖	mathematical	—	altRightRightUnit PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.downR Color.upR TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim	—	altRightRightUnit_eq_basis basis_eq_ofRat
coContrUnit_eq_basis 📖	mathematical	—	coContrUnit TensorSpecies.repDim Color complexLorentzTensor Color.down Color.up TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis	—	coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4 TensorSpecies.Tensor.fromPairT_apply_basis_repr
coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4 📖	mathematical	—	coContrUnit TensorSpecies.Tensor Color complexLorentzTensor Color.down Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Lorentz.complexCo Lorentz.complexCoBasisFin4 Lorentz.complexContr Lorentz.complexContrBasisFin4	—	coContrUnit_eq_complexCoBasis_complexContrBasis
coContrUnit_eq_complexCoBasis_complexContrBasis 📖	mathematical	—	coContrUnit TensorSpecies.Tensor Color complexLorentzTensor Color.down Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Lorentz.complexCo Lorentz.complexCoBasis Lorentz.complexContr Lorentz.complexContrBasis	—	coContrUnit_eq_fromPairT Lorentz.coContrUnitVal_expand_tmul
coContrUnit_eq_fromConstPair 📖	mathematical	—	coContrUnit TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.down Color.up Lorentz.coContrUnit	—	Lorentz.coContrUnit.eq_1
coContrUnit_eq_fromPairT 📖	mathematical	—	coContrUnit Color TensorSpecies.FD complexLorentzTensor Color.down Color.up TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Lorentz.coContrUnitVal	—	coContrUnit_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Lorentz.coContrUnit_apply_one
coContrUnit_eq_ofRat 📖	mathematical	—	coContrUnit PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.down Color.up TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim	—	coContrUnit_eq_basis basis_eq_ofRat
contrCoUnit_eq_basis 📖	mathematical	—	contrCoUnit TensorSpecies.repDim Color complexLorentzTensor Color.up Color.down TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis	—	contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4 TensorSpecies.Tensor.fromPairT_apply_basis_repr
contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4 📖	mathematical	—	contrCoUnit TensorSpecies.Tensor Color complexLorentzTensor Color.up Color.down IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Lorentz.complexContr Lorentz.complexContrBasisFin4 Lorentz.complexCo Lorentz.complexCoBasisFin4	—	contrCoUnit_eq_complexContrBasis_complexCoBasis
contrCoUnit_eq_complexContrBasis_complexCoBasis 📖	mathematical	—	contrCoUnit TensorSpecies.Tensor Color complexLorentzTensor Color.up Color.down IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Lorentz.complexContr Lorentz.complexContrBasis Lorentz.complexCo Lorentz.complexCoBasis	—	contrCoUnit_eq_fromPairT Lorentz.contrCoUnitVal_expand_tmul
contrCoUnit_eq_fromConstPair 📖	mathematical	—	contrCoUnit TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.up Color.down Lorentz.contrCoUnit	—	Lorentz.contrCoUnit.eq_1
contrCoUnit_eq_fromPairT 📖	mathematical	—	contrCoUnit Color TensorSpecies.FD complexLorentzTensor Color.up Color.down TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Lorentz.contrCoUnitVal	—	contrCoUnit_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Lorentz.contrCoUnit_apply_one
contrCoUnit_eq_ofRat 📖	mathematical	—	contrCoUnit PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.up Color.down TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim	—	contrCoUnit_eq_basis basis_eq_ofRat
leftAltLeftUnit_eq_basis 📖	mathematical	—	leftAltLeftUnit TensorSpecies.repDim Color complexLorentzTensor Color.upL Color.downL TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis	—	leftAltLeftUnit_eq_leftBasis_altLeftBasis TensorSpecies.Tensor.fromPairT_apply_basis_repr
leftAltLeftUnit_eq_fromConstPair 📖	mathematical	—	leftAltLeftUnit TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.upL Color.downL Fermion.leftAltLeftUnit	—	Fermion.leftAltLeftUnit.eq_1
leftAltLeftUnit_eq_fromPairT 📖	mathematical	—	leftAltLeftUnit Color TensorSpecies.FD complexLorentzTensor Color.upL Color.downL TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Fermion.leftAltLeftUnitVal	—	leftAltLeftUnit_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Fermion.leftAltLeftUnit_apply_one
leftAltLeftUnit_eq_leftBasis_altLeftBasis 📖	mathematical	—	leftAltLeftUnit TensorSpecies.Tensor Color complexLorentzTensor Color.upL Color.downL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Fermion.leftHanded Fermion.leftBasis Fermion.altLeftHanded Fermion.altLeftBasis	—	leftAltLeftUnit_eq_fromPairT Fermion.leftAltLeftUnitVal_expand_tmul
leftAltLeftUnit_eq_ofRat 📖	mathematical	—	leftAltLeftUnit PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.upL Color.downL TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim	—	leftAltLeftUnit_eq_basis basis_eq_ofRat
rightAltRightUnit_eq_basis 📖	mathematical	—	rightAltRightUnit TensorSpecies.repDim Color complexLorentzTensor Color.upR Color.downR TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis	—	rightAltRightUnit_eq_rightBasis_altRightBasis TensorSpecies.Tensor.fromPairT_apply_basis_repr
rightAltRightUnit_eq_fromConstPair 📖	mathematical	—	rightAltRightUnit TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.upR Color.downR Fermion.rightAltRightUnit	—	Fermion.rightAltRightUnit.eq_1
rightAltRightUnit_eq_fromPairT 📖	mathematical	—	rightAltRightUnit Color TensorSpecies.FD complexLorentzTensor Color.upR Color.downR TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Fermion.rightAltRightUnitVal	—	rightAltRightUnit_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Fermion.rightAltRightUnit_apply_one
rightAltRightUnit_eq_ofRat 📖	mathematical	—	rightAltRightUnit PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.upR Color.downR TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim	—	rightAltRightUnit_eq_basis basis_eq_ofRat
rightAltRightUnit_eq_rightBasis_altRightBasis 📖	mathematical	—	rightAltRightUnit TensorSpecies.Tensor Color complexLorentzTensor Color.upR Color.downR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Fermion.rightHanded Fermion.rightBasis Fermion.altRightHanded Fermion.altRightBasis	—	rightAltRightUnit_eq_fromPairT Fermion.rightAltRightUnitVal_expand_tmul

---

← Back to Index