Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems altLeftMetric_antisymm, altLeftMetric_contr_leftMetric, altRightMetric_antisymm, altRightMetric_contr_rightMetric, coMetric_contr_contrMetric, coMetric_symm, contrMetric_contr_coMetric, contrMetric_symm, leftMetric_antisymm, leftMetric_contr_altLeftMetric, rightMetric_antisymm, rightMetric_contr_altRightMetric	12
Total	12

complexLorentzTensor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
altLeftMetric_antisymm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self altLeftMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.instNeZeroNatRepDim altLeftMetric_eq_ofRat ofRat_basis_repr_apply
altLeftMetric_contr_leftMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downL Color.upL TensorSpecies.Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.contrT TensorSpecies.Tensor.contrT_decide TensorSpecies.τ TensorSpecies.Tensor.prodT TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self altLeftMetric leftMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond instDecidableEqColor altLeftLeftUnit	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.τ_τ_apply TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit
altRightMetric_antisymm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self altRightMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.instNeZeroNatRepDim altRightMetric_eq_ofRat ofRat_basis_repr_apply
altRightMetric_contr_rightMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downR Color.upR TensorSpecies.Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.contrT TensorSpecies.Tensor.contrT_decide TensorSpecies.τ TensorSpecies.Tensor.prodT TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self altRightMetric rightMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond instDecidableEqColor altRightRightUnit	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.τ_τ_apply TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit
coMetric_contr_contrMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.down Color.up TensorSpecies.Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.contrT TensorSpecies.Tensor.contrT_decide TensorSpecies.τ TensorSpecies.Tensor.prodT TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self coMetric contrMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond instDecidableEqColor coContrUnit	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.τ_τ_apply TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit
coMetric_symm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.down IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self coMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.instNeZeroNatRepDim coMetric_eq_ofRat ofRat_basis_repr_apply
contrMetric_contr_coMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.up Color.down TensorSpecies.Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.contrT TensorSpecies.Tensor.contrT_decide TensorSpecies.τ TensorSpecies.Tensor.prodT TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self contrMetric coMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond instDecidableEqColor contrCoUnit	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.τ_τ_apply TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit
contrMetric_symm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self contrMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.instNeZeroNatRepDim contrMetric_eq_ofRat ofRat_basis_repr_apply
leftMetric_antisymm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self leftMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.instNeZeroNatRepDim leftMetric_eq_ofRat ofRat_basis_repr_apply
leftMetric_contr_altLeftMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upL Color.downL TensorSpecies.Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.contrT TensorSpecies.Tensor.contrT_decide TensorSpecies.τ TensorSpecies.Tensor.prodT TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self leftMetric altLeftMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond instDecidableEqColor leftAltLeftUnit	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.τ_τ_apply TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit
rightMetric_antisymm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self rightMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.instNeZeroNatRepDim rightMetric_eq_ofRat ofRat_basis_repr_apply
rightMetric_contr_altRightMetric 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upR Color.downR TensorSpecies.Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.contrT TensorSpecies.Tensor.contrT_decide TensorSpecies.τ TensorSpecies.Tensor.prodT TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self rightMetric altRightMetric TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond instDecidableEqColor rightAltRightUnit	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.τ_τ_apply TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit

---

← Back to Index