Relations

📁 Source: PhysLean/Relativity/PauliMatrices/Relations.lean

Statistics

Metric	Count
Definitions	0
Theorems auliContrDown_pauliContr_mul_add, pauliCoDown_trace_pauliCo, pauliCo_contr_pauliContr, pauliCo_trace_pauliCoDown, pauliContr_mul_pauliContrDown_add	5
Total	5

PauliMatrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
auliContrDown_pauliContr_mul_add 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.downR complexLorentzTensor.Color.downL complexLorentzTensor.Color.upL complexLorentzTensor.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 pauliContrDown tensorial pauliMatrix TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond complexLorentzTensor.instDecidableEqColor complexLorentzTensor.contrMetric complexLorentzTensor.altRightRightUnit	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.repDim_τ TensorSpecies.instNeZeroNatRepDim TensorSpecies.Tensor.PermCond.inv_perserve_color pauliContrDown_ofRat toTensor_eq_ofRat complexLorentzTensor.prodT_ofRat_ofRat complexLorentzTensor.contrT_ofRat complexLorentzTensor.permT_ofRat complexLorentzTensor.altRightRightUnit_eq_ofRat complexLorentzTensor.contrMetric_eq_ofRat complexLorentzTensor.ofRat_basis_repr_apply PhysLean.RatComplexNum.toComplexNum_injective
pauliCoDown_trace_pauliCo 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.downR complexLorentzTensor.Color.downL complexLorentzTensor.Color.upL complexLorentzTensor.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 pauliCoDown pauliCo TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond complexLorentzTensor.instDecidableEqColor complexLorentzTensor.coMetric	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.repDim_τ TensorSpecies.instNeZeroNatRepDim pauliCoDown_eq_ofRat pauliCo_eq_ofRat complexLorentzTensor.prodT_ofRat_ofRat complexLorentzTensor.contrT_ofRat complexLorentzTensor.coMetric_eq_ofRat TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply complexLorentzTensor.ofRat_basis_repr_apply PhysLean.RatComplexNum.toComplexNum_injective
pauliCo_contr_pauliContr 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR complexLorentzTensor.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 pauliCo tensorial pauliMatrix TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond complexLorentzTensor.instDecidableEqColor complexLorentzTensor.leftMetric complexLorentzTensor.rightMetric	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.instNeZeroNatRepDim TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.Tensor.prodT_basis_repr_apply complexLorentzTensor.leftMetric_eq_ofRat complexLorentzTensor.rightMetric_eq_ofRat complexLorentzTensor.ofRat_basis_repr_apply PhysLean.RatComplexNum.ofNat_mul_toComplexNum TensorSpecies.Tensor.contrT_basis_repr_apply pauliCo_eq_ofRat toTensor_eq_ofRat complexLorentzTensor.contr_basis_ratComplexNum PhysLean.RatComplexNum.toComplexNum_injective
pauliCo_trace_pauliCoDown 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR complexLorentzTensor.Color.downR complexLorentzTensor.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 pauliCo pauliCoDown TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond complexLorentzTensor.instDecidableEqColor complexLorentzTensor.coMetric	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.repDim_τ TensorSpecies.instNeZeroNatRepDim pauliCoDown_eq_ofRat pauliCo_eq_ofRat complexLorentzTensor.prodT_ofRat_ofRat complexLorentzTensor.contrT_ofRat complexLorentzTensor.coMetric_eq_ofRat TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply complexLorentzTensor.ofRat_basis_repr_apply PhysLean.RatComplexNum.toComplexNum_injective
pauliContr_mul_pauliContrDown_add 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR complexLorentzTensor.Color.downR complexLorentzTensor.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 tensorial pauliMatrix pauliContrDown TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond complexLorentzTensor.instDecidableEqColor complexLorentzTensor.contrMetric complexLorentzTensor.leftAltLeftUnit	—	TensorSpecies.Tensor.contrT_decide TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensorial.self_toTensor_apply TensorSpecies.repDim_τ TensorSpecies.instNeZeroNatRepDim TensorSpecies.Tensor.PermCond.inv_perserve_color pauliContrDown_ofRat toTensor_eq_ofRat complexLorentzTensor.prodT_ofRat_ofRat complexLorentzTensor.contrT_ofRat complexLorentzTensor.permT_ofRat complexLorentzTensor.leftAltLeftUnit_eq_ofRat complexLorentzTensor.contrMetric_eq_ofRat complexLorentzTensor.ofRat_basis_repr_apply PhysLean.RatComplexNum.toComplexNum_injective

---

← Back to Index