Basic

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

Statistics

Metric	Count
Definitions altLeftMetric, altRightMetric, coMetric, contrMetric, leftMetric, rightMetric, termεL, termεL', termεR, termεR', termη, termη'	12
Theorems actionT_altLeftMetric, actionT_altRightMetric, actionT_coMetric, actionT_contrMetric, actionT_leftMetric, actionT_rightMetric, altLeftMetric_eq_altLeftBasis, altLeftMetric_eq_basis, altLeftMetric_eq_fromConstPair, altLeftMetric_eq_fromPairT, altLeftMetric_eq_ofRat, altRightMetric_eq_altRightBasis, altRightMetric_eq_basis, altRightMetric_eq_fromConstPair, altRightMetric_eq_fromPairT, altRightMetric_eq_ofRat, coMetric_eq_basis, coMetric_eq_complexCoBasis, coMetric_eq_complexCoBasisFin4, coMetric_eq_fromConstPair, coMetric_eq_fromPairT, coMetric_eq_ofRat, contrMetric_eq_basis, contrMetric_eq_complexContrBasis, contrMetric_eq_complexContrBasisFin4, contrMetric_eq_fromConstPair, contrMetric_eq_fromPairT, contrMetric_eq_ofRat, leftMetric_eq_basis, leftMetric_eq_fromConstPair, leftMetric_eq_fromPairT, leftMetric_eq_leftBasis, leftMetric_eq_ofRat, rightMetric_eq_basis, rightMetric_eq_fromConstPair, rightMetric_eq_fromPairT, rightMetric_eq_ofRat, rightMetric_eq_rightBasis	38
Total	50

complexLorentzTensor

Definitions

Name	Category	Theorems
altLeftMetric 📖	CompOp	9 math math: altLeftMetric_contr_leftMetric, altLeftMetric_eq_basis, altLeftMetric_antisymm, altLeftMetric_eq_fromPairT, altLeftMetric_eq_ofRat, leftMetric_contr_altLeftMetric, altLeftMetric_eq_fromConstPair, altLeftMetric_eq_altLeftBasis, actionT_altLeftMetric
altRightMetric 📖	CompOp	9 math math: altRightMetric_eq_fromConstPair, altRightMetric_eq_altRightBasis, altRightMetric_eq_ofRat, altRightMetric_eq_basis, altRightMetric_eq_fromPairT, altRightMetric_contr_rightMetric, altRightMetric_antisymm, actionT_altRightMetric, rightMetric_contr_altRightMetric
coMetric 📖	CompOp	12 math math: contrMetric_contr_coMetric, coMetric_symm, PauliMatrix.pauliCoDown_trace_pauliCo, coMetric_contr_contrMetric, coMetric_eq_ofRat, coMetric_eq_basis, actionT_coMetric, coMetric_eq_complexCoBasisFin4, coMetric_eq_complexCoBasis, coMetric_eq_fromPairT, coMetric_eq_fromConstPair, PauliMatrix.pauliCo_trace_pauliCoDown
contrMetric 📖	CompOp	12 math math: contrMetric_contr_coMetric, contrMetric_symm, contrMetric_eq_complexContrBasisFin4, contrMetric_eq_complexContrBasis, coMetric_contr_contrMetric, contrMetric_eq_fromPairT, actionT_contrMetric, contrMetric_eq_basis, PauliMatrix.auliContrDown_pauliContr_mul_add, contrMetric_eq_ofRat, PauliMatrix.pauliContr_mul_pauliContrDown_add, contrMetric_eq_fromConstPair
leftMetric 📖	CompOp	10 math math: PauliMatrix.pauliCo_contr_pauliContr, altLeftMetric_contr_leftMetric, leftMetric_contr_altLeftMetric, leftMetric_eq_basis, leftMetric_eq_leftBasis, leftMetric_antisymm, actionT_leftMetric, leftMetric_eq_fromPairT, leftMetric_eq_fromConstPair, leftMetric_eq_ofRat
rightMetric 📖	CompOp	10 math math: rightMetric_eq_basis, PauliMatrix.pauliCo_contr_pauliContr, rightMetric_eq_rightBasis, actionT_rightMetric, rightMetric_eq_ofRat, altRightMetric_contr_rightMetric, rightMetric_eq_fromConstPair, rightMetric_antisymm, rightMetric_eq_fromPairT, rightMetric_contr_altRightMetric
termεL 📖	CompOp	—
termεL' 📖	CompOp	—
termεR 📖	CompOp	—
termεR' 📖	CompOp	—
termη 📖	CompOp	—
termη' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
actionT_altLeftMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downL TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self altLeftMetric	—	TensorSpecies.metricTensor_invariant
actionT_altRightMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downR TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self altRightMetric	—	TensorSpecies.metricTensor_invariant
actionT_coMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.down TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self coMetric	—	TensorSpecies.metricTensor_invariant
actionT_contrMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.up TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self contrMetric	—	TensorSpecies.metricTensor_invariant
actionT_leftMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upL TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self leftMetric	—	TensorSpecies.metricTensor_invariant
actionT_rightMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upR TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self rightMetric	—	TensorSpecies.metricTensor_invariant
altLeftMetric_eq_altLeftBasis 📖	mathematical	—	altLeftMetric TensorSpecies.Tensor Color complexLorentzTensor Color.downL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Fermion.altLeftHanded Fermion.altLeftBasis	—	altLeftMetric_eq_fromPairT Fermion.altLeftMetricVal_expand_tmul
altLeftMetric_eq_basis 📖	mathematical	—	altLeftMetric TensorSpecies.Tensor Color complexLorentzTensor Color.downL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim altLeftMetric_eq_altLeftBasis TensorSpecies.Tensor.fromPairT_apply_basis_repr
altLeftMetric_eq_fromConstPair 📖	mathematical	—	altLeftMetric TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.downL Fermion.altLeftMetric	—	—
altLeftMetric_eq_fromPairT 📖	mathematical	—	altLeftMetric Color TensorSpecies.FD complexLorentzTensor Color.downL TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Fermion.altLeftMetricVal	—	altLeftMetric_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Fermion.altLeftMetric_apply_one
altLeftMetric_eq_ofRat 📖	mathematical	—	altLeftMetric PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.downL TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim PhysLean.RatComplexNum.instAddCommGroup	—	TensorSpecies.instNeZeroNatRepDim altLeftMetric_eq_basis basis_eq_ofRat
altRightMetric_eq_altRightBasis 📖	mathematical	—	altRightMetric TensorSpecies.Tensor Color complexLorentzTensor Color.downR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Fermion.altRightHanded Fermion.altRightBasis	—	altRightMetric_eq_fromPairT Fermion.altRightMetricVal_expand_tmul
altRightMetric_eq_basis 📖	mathematical	—	altRightMetric TensorSpecies.Tensor Color complexLorentzTensor Color.downR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim altRightMetric_eq_altRightBasis TensorSpecies.Tensor.fromPairT_apply_basis_repr
altRightMetric_eq_fromConstPair 📖	mathematical	—	altRightMetric TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.downR Fermion.altRightMetric	—	—
altRightMetric_eq_fromPairT 📖	mathematical	—	altRightMetric Color TensorSpecies.FD complexLorentzTensor Color.downR TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Fermion.altRightMetricVal	—	altRightMetric_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Fermion.altRightMetric_apply_one
altRightMetric_eq_ofRat 📖	mathematical	—	altRightMetric PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.downR TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim PhysLean.RatComplexNum.instAddCommGroup	—	TensorSpecies.instNeZeroNatRepDim altRightMetric_eq_basis basis_eq_ofRat
coMetric_eq_basis 📖	mathematical	—	coMetric TensorSpecies.Tensor Color complexLorentzTensor Color.down IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim coMetric_eq_complexCoBasisFin4 TensorSpecies.Tensor.fromPairT_apply_basis_repr
coMetric_eq_complexCoBasis 📖	mathematical	—	coMetric TensorSpecies.Tensor Color complexLorentzTensor Color.down IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Lorentz.complexCo Lorentz.complexCoBasis	—	coMetric_eq_fromPairT Lorentz.coMetricVal_expand_tmul
coMetric_eq_complexCoBasisFin4 📖	mathematical	—	coMetric TensorSpecies.Tensor Color complexLorentzTensor Color.down IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Lorentz.complexCo Lorentz.complexCoBasisFin4	—	coMetric_eq_complexCoBasis
coMetric_eq_fromConstPair 📖	mathematical	—	coMetric TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.down Lorentz.coMetric	—	Lorentz.coMetric.eq_1
coMetric_eq_fromPairT 📖	mathematical	—	coMetric Color TensorSpecies.FD complexLorentzTensor Color.down TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Lorentz.coMetricVal	—	coMetric_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Lorentz.coMetric_apply_one
coMetric_eq_ofRat 📖	mathematical	—	coMetric PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.down TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim PhysLean.RatComplexNum.instAddCommGroup	—	TensorSpecies.instNeZeroNatRepDim coMetric_eq_basis basis_eq_ofRat
contrMetric_eq_basis 📖	mathematical	—	contrMetric TensorSpecies.Tensor Color complexLorentzTensor Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim contrMetric_eq_complexContrBasisFin4 TensorSpecies.Tensor.fromPairT_apply_basis_repr
contrMetric_eq_complexContrBasis 📖	mathematical	—	contrMetric TensorSpecies.Tensor Color complexLorentzTensor Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Lorentz.complexContr Lorentz.complexContrBasis	—	contrMetric_eq_fromPairT Lorentz.contrMetricVal_expand_tmul
contrMetric_eq_complexContrBasisFin4 📖	mathematical	—	contrMetric TensorSpecies.Tensor Color complexLorentzTensor Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Lorentz.complexContr Lorentz.complexContrBasisFin4	—	contrMetric_eq_complexContrBasis
contrMetric_eq_fromConstPair 📖	mathematical	—	contrMetric TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.up Lorentz.contrMetric	—	Lorentz.contrMetric.eq_1
contrMetric_eq_fromPairT 📖	mathematical	—	contrMetric Color TensorSpecies.FD complexLorentzTensor Color.up TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Lorentz.contrMetricVal	—	contrMetric_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Lorentz.contrMetric_apply_one
contrMetric_eq_ofRat 📖	mathematical	—	contrMetric PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.up TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim PhysLean.RatComplexNum.instAddCommGroup	—	TensorSpecies.instNeZeroNatRepDim contrMetric_eq_basis basis_eq_ofRat
leftMetric_eq_basis 📖	mathematical	—	leftMetric TensorSpecies.Tensor Color complexLorentzTensor Color.upL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim leftMetric_eq_leftBasis TensorSpecies.Tensor.fromPairT_apply_basis_repr
leftMetric_eq_fromConstPair 📖	mathematical	—	leftMetric TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.upL Fermion.leftMetric	—	—
leftMetric_eq_fromPairT 📖	mathematical	—	leftMetric Color TensorSpecies.FD complexLorentzTensor Color.upL TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Fermion.leftMetricVal	—	leftMetric_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Fermion.leftMetric_apply_one
leftMetric_eq_leftBasis 📖	mathematical	—	leftMetric TensorSpecies.Tensor Color complexLorentzTensor Color.upL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Fermion.leftHanded Fermion.leftBasis	—	leftMetric_eq_fromPairT Fermion.leftMetricVal_expand_tmul
leftMetric_eq_ofRat 📖	mathematical	—	leftMetric PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.upL TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim PhysLean.RatComplexNum.instAddCommGroup	—	TensorSpecies.instNeZeroNatRepDim leftMetric_eq_basis basis_eq_ofRat
rightMetric_eq_basis 📖	mathematical	—	rightMetric TensorSpecies.Tensor Color complexLorentzTensor Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim rightMetric_eq_rightBasis TensorSpecies.Tensor.fromPairT_apply_basis_repr
rightMetric_eq_fromConstPair 📖	mathematical	—	rightMetric TensorSpecies.Tensor.fromConstPair Color complexLorentzTensor Color.upR Fermion.rightMetric	—	—
rightMetric_eq_fromPairT 📖	mathematical	—	rightMetric Color TensorSpecies.FD complexLorentzTensor Color.upR TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.fromPairT Fermion.rightMetricVal	—	rightMetric_eq_fromConstPair TensorSpecies.Tensor.fromConstPair.eq_1 Fermion.rightMetric_apply_one
rightMetric_eq_ofRat 📖	mathematical	—	rightMetric PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor Color complexLorentzTensor Color.upR TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim PhysLean.RatComplexNum.instAddCommGroup	—	TensorSpecies.instNeZeroNatRepDim rightMetric_eq_basis basis_eq_ofRat
rightMetric_eq_rightBasis 📖	mathematical	—	rightMetric TensorSpecies.Tensor Color complexLorentzTensor Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.FD TensorSpecies.Tensor.fromPairT Fermion.rightHanded Fermion.rightBasis	—	rightMetric_eq_fromPairT Fermion.rightMetricVal_expand_tmul

---

← Back to Index