OfRat

📁 Source: PhysLean/Relativity/Tensors/ComplexTensor/OfRat.lean

Statistics

Metric	Count
Definitions ofRat	1
Theorems basis_eq_ofRat, contrT_ofRat, contrT_ofRat_eq_sum_dropPairSection, contr_basis_ratComplexNum, ofRat_basis_repr_apply, permT_ofRat, prodT_ofRat_ofRat	7
Total	8

complexLorentzTensor

Definitions

Name	Category	Theorems
ofRat 📖	CompOp	22 math math: contrT_ofRat_eq_sum_dropPairSection, altLeftLeftUnit_eq_ofRat, PauliMatrix.pauliCoDown_eq_ofRat, altLeftMetric_eq_ofRat, ofRat_basis_repr_apply, permT_ofRat, coContrUnit_eq_ofRat, altRightMetric_eq_ofRat, PauliMatrix.pauliContrDown_ofRat, leftAltLeftUnit_eq_ofRat, altRightRightUnit_eq_ofRat, coMetric_eq_ofRat, basis_eq_ofRat, contrCoUnit_eq_ofRat, rightMetric_eq_ofRat, rightAltRightUnit_eq_ofRat, contrT_ofRat, leftMetric_eq_ofRat, contrMetric_eq_ofRat, prodT_ofRat_ofRat, PauliMatrix.toTensor_eq_ofRat, PauliMatrix.pauliCo_eq_ofRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_eq_ofRat 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx Color complexLorentzTensor TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum ofRat TensorSpecies.repDim	—	ofRat_basis_repr_apply PhysLean.RatComplexNum.toComplexNum.eq_1
contrT_ofRat 📖	mathematical	TensorSpecies.τ Color complexLorentzTensor	TensorSpecies.Tensor TensorSpecies.Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.contrT PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor.ComponentIdx ofRat TensorSpecies.repDim TensorSpecies.Tensor.ComponentIdx.DropPairSection TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv TensorSpecies.repDim_τ	—	TensorSpecies.repDim_τ contrT_ofRat_eq_sum_dropPairSection TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv_apply_fst TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv_apply_snd
contrT_ofRat_eq_sum_dropPairSection 📖	mathematical	TensorSpecies.τ Color complexLorentzTensor	TensorSpecies.Tensor TensorSpecies.Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.contrT PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor.ComponentIdx ofRat TensorSpecies.Tensor.ComponentIdx.DropPairSection PhysLean.RatComplexNum.instMul TensorSpecies.repDim	—	TensorSpecies.Tensor.contrT_basis_repr_apply contr_basis_ratComplexNum ofRat_basis_repr_apply
contr_basis_ratComplexNum 📖	mathematical	—	TensorSpecies.castToField Color complexLorentzTensor IndexNotation.OverColor.Discrete.pairτ TensorSpecies.FD TensorSpecies.τ TensorSpecies.contr TensorSpecies.repDim TensorSpecies.basis PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum	—	Fermion.leftAltContraction_basis Fermion.altLeftContraction_basis Fermion.rightAltContraction_basis Lorentz.contrCoContraction_basis
ofRat_basis_repr_apply 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx Color complexLorentzTensor TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum ofRat	—	—
permT_ofRat 📖	mathematical	TensorSpecies.Tensor.PermCond Color	TensorSpecies.Tensor complexLorentzTensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.permT PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor.ComponentIdx ofRat TensorSpecies.repDim TensorSpecies.Tensor.PermCond.inv TensorSpecies.Tensor.PermCond.inv_perserve_color	—	TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply ofRat_basis_repr_apply
prodT_ofRat_ofRat 📖	mathematical	—	TensorSpecies.Tensor Color complexLorentzTensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.prodT PhysLean.RatComplexNum PhysLean.RatComplexNum.instRing PhysLean.RatComplexNum.toComplexNum TensorSpecies.Tensor.ComponentIdx ofRat PhysLean.RatComplexNum.instMul TensorSpecies.Tensor.ComponentIdx.prodEquiv	—	TensorSpecies.Tensor.prodT_basis_repr_apply ofRat_basis_repr_apply

---

← Back to Index