Symm

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

Statistics

Metric	Count
Definitions	0
Theorems altLeftLeftUnit_symm, altRightRightUnit_symm, coContrUnit_symm, contrCoUnit_symm, leftAltLeftUnit_symm, rightAltRightUnit_symm	6
Total	6

complexLorentzTensor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
altLeftLeftUnit_symm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downL Color.upL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self altLeftLeftUnit TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond leftAltLeftUnit	—	TensorSpecies.Tensor.PermCond.auto altLeftLeftUnit.eq_1 TensorSpecies.τ_τ_apply TensorSpecies.unitTensor_eq_permT_dual
altRightRightUnit_symm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.downR Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self altRightRightUnit TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond rightAltRightUnit	—	TensorSpecies.Tensor.PermCond.auto altRightRightUnit.eq_1 TensorSpecies.τ_τ_apply TensorSpecies.unitTensor_eq_permT_dual
coContrUnit_symm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.down Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self coContrUnit TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond contrCoUnit	—	TensorSpecies.Tensor.PermCond.auto coContrUnit.eq_1 TensorSpecies.τ_τ_apply TensorSpecies.unitTensor_eq_permT_dual
contrCoUnit_symm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.up Color.down IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self contrCoUnit TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond coContrUnit	—	TensorSpecies.Tensor.PermCond.auto contrCoUnit.eq_1 TensorSpecies.τ_τ_apply TensorSpecies.unitTensor_eq_permT_dual
leftAltLeftUnit_symm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upL Color.downL IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self leftAltLeftUnit TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond altLeftLeftUnit	—	TensorSpecies.Tensor.PermCond.auto leftAltLeftUnit.eq_1 TensorSpecies.τ_τ_apply TensorSpecies.unitTensor_eq_permT_dual
rightAltRightUnit_symm 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor Color.upR Color.downR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.self rightAltRightUnit TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond altRightRightUnit	—	TensorSpecies.Tensor.PermCond.auto rightAltRightUnit.eq_1 TensorSpecies.τ_τ_apply TensorSpecies.unitTensor_eq_permT_dual

---

← Back to Index