Constructors

📁 Source: PhysLean/Relativity/Tensors/Constructors.lean

Statistics

Metric	Count
Definitions fromSingleP, fromConst, fromConstPair, fromConstTriple, fromPairT, fromPairTContr, fromSingleT, fromSingleTContrFromPairT, fromTripleT	9
Theorems actionT_fromConst, actionT_fromConstPair, actionT_fromConstTriple, actionT_fromPairT, actionT_fromSingleT, actionT_fromTripleT, contrT_fromSingleT_fromPairT, contrT_fromSingleT_fromSingleT, fromConstPair_braid, fromConstPair_whiskerLeft, fromPairTContr_tmul_tmul, fromPairT_apply_basis_repr, fromPairT_basis_repr, fromPairT_comm, fromPairT_contr_fromPairT_eq_fromPairTContr, fromPairT_contr_fromPairT_eq_fromPairTContr_tmul, fromPairT_map_right, fromPairT_tmul, fromSingleTContrFromPairT_tmul, fromSingleT_contr_fromPairT_tmul, fromSingleT_eq_pureT, fromSingleT_map, fromSingleT_symm_pure, fromTripleT_apply_basis, fromTripleT_basis_repr, fromTripleT_tmul	26
Total	35

TensorSpecies.Tensor

Definitions

Name	Category	Theorems
fromConst 📖	CompOp	1 math math: actionT_fromConst
fromConstPair 📖	CompOp	17 math math: complexLorentzTensor.altRightMetric_eq_fromConstPair, complexLorentzTensor.altRightRightUnit_eq_fromConstPair, complexLorentzTensor.contrCoUnit_eq_fromConstPair, realLorentzTensor.coMetric_eq_fromConstPair, complexLorentzTensor.altLeftMetric_eq_fromConstPair, complexLorentzTensor.leftAltLeftUnit_eq_fromConstPair, complexLorentzTensor.rightMetric_eq_fromConstPair, complexLorentzTensor.rightAltRightUnit_eq_fromConstPair, fromConstPair_whiskerLeft, actionT_fromConstPair, fromConstPair_braid, complexLorentzTensor.leftMetric_eq_fromConstPair, realLorentzTensor.contrMetric_eq_fromConstPair, complexLorentzTensor.coContrUnit_eq_fromConstPair, complexLorentzTensor.coMetric_eq_fromConstPair, complexLorentzTensor.altLeftLeftUnit_eq_fromConstPair, complexLorentzTensor.contrMetric_eq_fromConstPair
fromConstTriple 📖	CompOp	2 math math: PauliMatrix.toTensor_eq_asConsTensor, actionT_fromConstTriple
fromPairT 📖	CompOp	41 math math: contrT_fromSingleT_fromPairT, complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis, complexLorentzTensor.rightAltRightUnit_eq_fromPairT, complexLorentzTensor.altLeftMetric_eq_fromPairT, complexLorentzTensor.leftAltLeftUnit_eq_leftBasis_altLeftBasis, complexLorentzTensor.rightAltRightUnit_eq_rightBasis_altRightBasis, complexLorentzTensor.contrMetric_eq_complexContrBasisFin4, complexLorentzTensor.altRightMetric_eq_altRightBasis, realLorentzTensor.contrMetric_eq_fromPairT, complexLorentzTensor.rightMetric_eq_rightBasis, complexLorentzTensor.contrMetric_eq_complexContrBasis, fromPairTContr_tmul_tmul, complexLorentzTensor.leftAltLeftUnit_eq_fromPairT, fromPairT_basis_repr, fromPairT_apply_basis_repr, complexLorentzTensor.contrMetric_eq_fromPairT, complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4, complexLorentzTensor.leftMetric_eq_leftBasis, complexLorentzTensor.altRightRightUnit_eq_fromPairT, fromPairT_comm, actionT_fromPairT, complexLorentzTensor.altRightMetric_eq_fromPairT, complexLorentzTensor.altRightRightUnit_eq_altRightBasis_rightBasis, complexLorentzTensor.altLeftLeftUnit_eq_altLeftBasis_leftBasis, complexLorentzTensor.coContrUnit_eq_fromPairT, complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4, realLorentzTensor.coMetric_eq_fromPairT, fromPairT_contr_fromPairT_eq_fromPairTContr, complexLorentzTensor.contrCoUnit_eq_fromPairT, complexLorentzTensor.leftMetric_eq_fromPairT, complexLorentzTensor.rightMetric_eq_fromPairT, complexLorentzTensor.coMetric_eq_complexCoBasisFin4, complexLorentzTensor.altLeftMetric_eq_altLeftBasis, fromPairT_contr_fromPairT_eq_fromPairTContr_tmul, complexLorentzTensor.coMetric_eq_complexCoBasis, complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis, complexLorentzTensor.coMetric_eq_fromPairT, complexLorentzTensor.altLeftLeftUnit_eq_fromPairT, fromPairT_map_right, fromPairT_tmul, fromSingleT_contr_fromPairT_tmul
fromPairTContr 📖	CompOp	5 math math: TensorSpecies.permT_fromPairTContr_metric_metric, fromPairTContr_tmul_tmul, TensorSpecies.fromPairTContr_metric_metric_eq_permT_unit, fromPairT_contr_fromPairT_eq_fromPairTContr, fromPairT_contr_fromPairT_eq_fromPairTContr_tmul
fromSingleT 📖	CompOp	11 math math: contrT_fromSingleT_fromPairT, fromTripleT_tmul, contrT_fromSingleT_fromSingleT, TensorSpecies.unit_fromSingleTContrFromPairT_eq_fromSingleT, fromSingleT_map, fromSingleT_eq_pureT, fromSingleTContrFromPairT_tmul, fromSingleT_symm_pure, fromPairT_tmul, actionT_fromSingleT, fromSingleT_contr_fromPairT_tmul
fromSingleTContrFromPairT 📖	CompOp	4 math math: contrT_fromSingleT_fromPairT, TensorSpecies.unit_fromSingleTContrFromPairT_eq_fromSingleT, fromSingleTContrFromPairT_tmul, fromSingleT_contr_fromPairT_tmul
fromTripleT 📖	CompOp	4 math math: actionT_fromTripleT, fromTripleT_apply_basis, fromTripleT_tmul, fromTripleT_basis_repr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
actionT_fromConst 📖	mathematical	—	TensorSpecies.Tensor actionT fromConst	—	—
actionT_fromConstPair 📖	mathematical	—	TensorSpecies.Tensor actionT fromConstPair	—	fromConstPair.eq_1 actionT_fromPairT
actionT_fromConstTriple 📖	mathematical	—	TensorSpecies.Tensor actionT fromConstTriple	—	fromConstTriple.eq_1 actionT_fromTripleT
actionT_fromPairT 📖	mathematical	—	TensorSpecies.Tensor actionT TensorSpecies.FD IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromPairT	—	actionT_zero fromPairT_tmul permT_equivariant prodT_equivariant actionT_fromSingleT actionT_add
actionT_fromSingleT 📖	mathematical	—	TensorSpecies.Tensor actionT TensorSpecies.FD IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromSingleT	—	fromSingleT_eq_pureT actionT_pure
actionT_fromTripleT 📖	mathematical	—	TensorSpecies.Tensor actionT TensorSpecies.FD IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromTripleT	—	actionT_zero fromTripleT_tmul permT_equivariant prodT_equivariant actionT_fromSingleT actionT_add
contrT_fromSingleT_fromPairT 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F contrT prodT TensorSpecies.FD fromSingleT fromPairT permT PermCond fromSingleTContrFromPairT	—	fromSingleT_contr_fromPairT_tmul
contrT_fromSingleT_fromSingleT 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F contrT prodT TensorSpecies.FD fromSingleT IndexNotation.OverColor.Discrete.pairτ TensorSpecies.contr Pure.toTensor Pure	—	fromSingleT_eq_pureT prodT_pure contrT_pure Pure.prodP_apply_finSumFinEquiv
fromConstPair_braid 📖	mathematical	—	fromConstPair TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT	—	fromConstPair.eq_1 fromPairT_comm
fromConstPair_whiskerLeft 📖	mathematical	—	fromConstPair TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT	—	fromConstPair.eq_1 fromPairT_map_right
fromPairTContr_tmul_tmul 📖	mathematical	—	fromPairTContr TensorSpecies.FD TensorSpecies.τ TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F IndexNotation.OverColor.Discrete.pairτ TensorSpecies.contr fromPairT	—	fromPairTContr.eq_1
fromPairT_apply_basis_repr 📖	mathematical	—	TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromPairT TensorSpecies.repDim TensorSpecies.basis ComponentIdx basis	—	fromPairT_basis_repr
fromPairT_basis_repr 📖	mathematical	—	ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis TensorSpecies.FD fromPairT TensorSpecies.repDim TensorSpecies.basis	—	fromPairT_tmul fromSingleT_eq_pureT prodT_pure permT_pure basis_repr_pure Pure.prodP_apply_finSumFinEquiv
fromPairT_comm 📖	mathematical	—	TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromPairT permT	—	fromPairT_tmul prodSwapMap_permCond prodT_swap PermCond.comp permT_permT permT.congr_simp
fromPairT_contr_fromPairT_eq_fromPairTContr 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F contrT prodT TensorSpecies.FD fromPairT permT PermCond fromPairTContr	—	fromPairT_contr_fromPairT_eq_fromPairTContr_tmul
fromPairT_contr_fromPairT_eq_fromPairTContr_tmul 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F contrT prodT TensorSpecies.FD fromPairT permT PermCond fromPairTContr	—	fromPairT_tmul prodLeftMap_permCond prodT_permT_left prodRightMap_permCond prodT_permT_right PermCond.comp permT_permT prodRightMap_id prodLeftMap_id permT.congr_simp Pure.permCond_dropPairOfMap contrT_permT Pure.dropPairEmb_permCond_prod prodT_contrT_snd prodSwapMap_permCond prodT_swap prodAssocMap'_permCond prodT_assoc' prodAssocMap_permCond prodT_assoc permT_congr_eq_id Pure.dropPairOfMap_id contrT_fromSingleT_fromSingleT Pure.prodP_zero_right_permCond prodT_default_right fromPairTContr_tmul_tmul
fromPairT_map_right 📖	mathematical	—	TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromPairT permT PermCond	—	fromPairT_tmul fromSingleT_map prodRightMap_permCond prodT_permT_right PermCond.comp permT_permT prodRightMap_id permT.congr_simp
fromPairT_tmul 📖	mathematical	—	TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromPairT permT prodT fromSingleT	—	—
fromSingleTContrFromPairT_tmul 📖	mathematical	—	fromSingleTContrFromPairT TensorSpecies.FD TensorSpecies.τ TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F IndexNotation.OverColor.Discrete.pairτ TensorSpecies.contr fromSingleT	—	fromSingleTContrFromPairT.eq_1
fromSingleT_contr_fromPairT_tmul 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F contrT prodT TensorSpecies.FD fromSingleT fromPairT permT PermCond fromSingleTContrFromPairT	—	prodSwapMap_permCond Pure.dropPairEmb_permCond_prod prodT_swap prodT_contrT_snd Pure.permCond_dropPairOfMap contrT_permT PermCond.comp permT_permT fromPairT_tmul prodRightMap_permCond prodAssocMap'_permCond prodT_permT_right prodT_assoc' permT_congr prodRightMap_id Pure.dropPairOfMap.congr_simp contrT_fromSingleT_fromSingleT fromSingleTContrFromPairT_tmul Pure.prodP_zero_right_permCond permT.congr_simp prodT_default_right
fromSingleT_eq_pureT 📖	mathematical	—	TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromSingleT Pure.toTensor	—	fromSingleT_symm_pure
fromSingleT_map 📖	mathematical	—	TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromSingleT permT PermCond	—	fromSingleT_eq_pureT permT_pure
fromSingleT_symm_pure 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.FD IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromSingleT Pure.toTensor Pure Pure.fromSingleP	—	IndexNotation.OverColor.forgetLiftApp_hom_hom_apply_eq IndexNotation.OverColor.Hom.toEquiv_comp_inv_apply IndexNotation.OverColor.lift.map_tprod Pure.congr_right
fromTripleT_apply_basis 📖	mathematical	—	TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromTripleT TensorSpecies.repDim TensorSpecies.basis ComponentIdx basis	—	fromTripleT_basis_repr
fromTripleT_basis_repr 📖	mathematical	—	ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis TensorSpecies.FD fromTripleT TensorSpecies.repDim TensorSpecies.basis	—	fromTripleT_tmul fromSingleT_eq_pureT prodT_pure permT_pure basis_repr_pure Pure.prodP_apply_finSumFinEquiv
fromTripleT_tmul 📖	mathematical	—	TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromTripleT permT prodT fromSingleT	—	—

TensorSpecies.Tensor.Pure

Definitions

Name	Category	Theorems
fromSingleP 📖	CompOp	1 math math: TensorSpecies.Tensor.fromSingleT_symm_pure

---

← Back to Index