ToTensor

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

Statistics

Metric	Count
Definitions indexEquiv, pauliCo, pauliCoDown, pauliContrDown, tensorial, termσ___, «termσ^^^», «termσ^__», «termσ_^^»	9
Theorems pauliCoDown_eq_ofRat, pauliCo_eq_ofRat, pauliContrDown_ofRat, smul_eq_self, smul_pauliCo, smul_pauliCoDown, smul_pauliContrDown, toTensor_basis_expand, toTensor_eq_asConsTensor, toTensor_eq_ofRat, toTensor_smul_eq_self, toTensor_symm_apply, toTensor_symm_basis	13
Total	22

PauliMatrix

Definitions

Name	Category	Theorems
indexEquiv 📖	CompOp	1 math math: toTensor_symm_apply
pauliCo 📖	CompOp	5 math math: pauliCo_contr_pauliContr, pauliCoDown_trace_pauliCo, smul_pauliCo, pauliCo_eq_ofRat, pauliCo_trace_pauliCoDown
pauliCoDown 📖	CompOp	4 math math: smul_pauliCoDown, pauliCoDown_eq_ofRat, pauliCoDown_trace_pauliCo, pauliCo_trace_pauliCoDown
pauliContrDown 📖	CompOp	4 math math: pauliContrDown_ofRat, smul_pauliContrDown, auliContrDown_pauliContr_mul_add, pauliContr_mul_pauliContrDown_add
tensorial 📖	CompOp	10 math math: pauliCo_contr_pauliContr, toTensor_smul_eq_self, toTensor_symm_apply, smul_eq_self, toTensor_symm_basis, toTensor_basis_expand, auliContrDown_pauliContr_mul_add, toTensor_eq_asConsTensor, toTensor_eq_ofRat, pauliContr_mul_pauliContrDown_add
termσ___ 📖	CompOp	—
«termσ^^^» 📖	CompOp	—
«termσ^__» 📖	CompOp	—
«termσ_^^» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pauliCoDown_eq_ofRat 📖	mathematical	—	pauliCoDown PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.downR complexLorentzTensor.Color.downL TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F complexLorentzTensor.ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim pauliCoDown.eq_1 TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.Tensor.contrT_basis_repr_apply TensorSpecies.Tensorial.self_toTensor_apply complexLorentzTensor.contr_basis_ratComplexNum TensorSpecies.Tensor.prodT_basis_repr_apply complexLorentzTensor.altLeftMetric_eq_ofRat complexLorentzTensor.ofRat_basis_repr_apply pauliCo_eq_ofRat complexLorentzTensor.altRightMetric_eq_ofRat PhysLean.RatComplexNum.toComplexNum_injective
pauliCo_eq_ofRat 📖	mathematical	—	pauliCo PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F complexLorentzTensor.ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim pauliCo.eq_1 TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.Tensor.contrT_basis_repr_apply TensorSpecies.Tensorial.self_toTensor_apply complexLorentzTensor.contr_basis_ratComplexNum TensorSpecies.Tensor.prodT_basis_repr_apply complexLorentzTensor.coMetric_eq_ofRat complexLorentzTensor.ofRat_basis_repr_apply toTensor_eq_ofRat PhysLean.RatComplexNum.toComplexNum_injective
pauliContrDown_ofRat 📖	mathematical	—	pauliContrDown PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.downR complexLorentzTensor.Color.downL TensorSpecies.Tensor.ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F complexLorentzTensor.ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim pauliContrDown.eq_1 TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply TensorSpecies.Tensor.contrT_basis_repr_apply TensorSpecies.Tensorial.self_toTensor_apply complexLorentzTensor.contr_basis_ratComplexNum TensorSpecies.Tensor.prodT_basis_repr_apply complexLorentzTensor.altLeftMetric_eq_ofRat complexLorentzTensor.ofRat_basis_repr_apply toTensor_eq_ofRat complexLorentzTensor.altRightMetric_eq_ofRat PhysLean.RatComplexNum.toComplexNum_injective
smul_eq_self 📖	mathematical	—	TensorSpecies.Tensorial.smulAction complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR tensorial pauliMatrix	—	TensorSpecies.Tensorial.smul_eq toTensor_eq_asConsTensor TensorSpecies.Tensor.actionT_fromConstTriple
smul_pauliCo 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self pauliCo	—	TensorSpecies.Tensor.permT_equivariant TensorSpecies.Tensor.contrT_equivariant TensorSpecies.Tensor.prodT_equivariant TensorSpecies.Tensorial.self_toTensor_apply toTensor_smul_eq_self complexLorentzTensor.actionT_coMetric
smul_pauliCoDown 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.downR complexLorentzTensor.Color.downL TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self pauliCoDown	—	TensorSpecies.Tensor.permT_equivariant TensorSpecies.Tensor.contrT_equivariant TensorSpecies.Tensor.prodT_equivariant TensorSpecies.Tensorial.self_toTensor_apply smul_pauliCo complexLorentzTensor.actionT_altLeftMetric complexLorentzTensor.actionT_altRightMetric
smul_pauliContrDown 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.downR complexLorentzTensor.Color.downL TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self pauliContrDown	—	TensorSpecies.Tensor.permT_equivariant TensorSpecies.Tensor.contrT_equivariant TensorSpecies.Tensor.prodT_equivariant TensorSpecies.Tensorial.self_toTensor_apply toTensor_smul_eq_self complexLorentzTensor.actionT_altLeftMetric complexLorentzTensor.actionT_altRightMetric
toTensor_basis_expand 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor tensorial pauliMatrix TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim toTensor_symm_basis
toTensor_eq_asConsTensor 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor tensorial pauliMatrix TensorSpecies.Tensor.fromConstTriple asConsTensor	—	TensorSpecies.Tensor.fromConstTriple.eq_1 asConsTensor_apply_one asTensor_expand TensorSpecies.instNeZeroNatRepDim toTensor_basis_expand Lorentz.complexContrBasisFin4_apply_zero Lorentz.complexContrBasisFin4_apply_one Lorentz.complexContrBasisFin4_apply_two Lorentz.complexContrBasisFin4_apply_three complexLorentzTensor.basis_up_eq complexLorentzTensor.basis_upL_eq complexLorentzTensor.basis_upR_eq TensorSpecies.Tensor.fromTripleT_apply_basis
toTensor_eq_ofRat 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor tensorial pauliMatrix PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor.ComponentIdx complexLorentzTensor.ofRat TensorSpecies.repDim TensorSpecies.instNeZeroNatRepDim	—	TensorSpecies.instNeZeroNatRepDim toTensor_basis_expand complexLorentzTensor.basis_eq_ofRat complexLorentzTensor.ofRat_basis_repr_apply PhysLean.RatComplexNum.I_mul_toComplexNum PhysLean.RatComplexNum.toComplexNum_injective
toTensor_smul_eq_self 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self TensorSpecies.Tensorial.toTensor tensorial pauliMatrix	—	toTensor_eq_asConsTensor TensorSpecies.Tensor.actionT_fromConstTriple
toTensor_symm_apply 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor tensorial TensorSpecies.Tensor.ComponentIdx indexEquiv TensorSpecies.repDim TensorSpecies.Tensor.basis	—	—
toTensor_symm_basis 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor tensorial TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim	—	toTensor_symm_apply

---

← Back to Index