| Name | Category | Theorems |
|---|
F 📖 | CompOp | 266 mathmath: realLorentzTensor.prodT_toComplex, Tensorial.basis_map_prod, complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection, complexLorentzTensor.rightMetric_eq_basis, complexLorentzTensor.contrMetric_contr_coMetric, Tensor.prodT_basis_repr_apply, PauliMatrix.pauliCo_contr_pauliContr, Tensor.contrT_fromSingleT_fromPairT, dual_unitTensor_eq_permT_unitTensor, Tensor.permT_basis_repr_symm_apply, Tensor.Pure.μ_toTensor_tmul_toTensor, Tensor.actionT_smul, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, complexLorentzTensor.coContrUnit_eq_basis, PauliMatrix.smul_pauliCoDown, complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis, complexLorentzTensor.altLeftLeftUnit_eq_ofRat, contrT_unitTensor_dual_single, complexLorentzTensor.altLeftMetric_contr_leftMetric, Lorentz.CoVector.toTensor_symm_pure, complexLorentzTensor.altLeftMetric_eq_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Lorentz.CoVector.tensor_basis_repr_toTensor_apply, Tensor.contrT_congr, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, complexLorentzTensor.rightAltRightUnit_eq_fromPairT, realLorentzTensor.toComplex_injective, realLorentzTensor.contrT_toComplex, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, complexLorentzTensor.contrMetric_symm, complexLorentzTensor.altLeftMetric_antisymm, castFin0ToField_tprod, SpaceTime.distTensorDeriv_toTensor_basis_repr, PauliMatrix.toTensor_smul_eq_self, PauliMatrix.pauliCoDown_eq_ofRat, Tensor.contrT_comm, complexLorentzTensor.altLeftMetric_eq_fromPairT, complexLorentzTensor.altLeftMetric_eq_ofRat, Tensor.permT_id_self, metricTensor_congr, Tensor.Pure.evalP_update_smul, Tensor.permT_equivariant, complexLorentzTensor.rightAltRightUnit_eq_basis, Lorentz.Vector.toTensor_basis_eq_tensor_basis, Tensor.basis_repr_pure, complexLorentzTensor.leftMetric_contr_altLeftMetric, Tensorial.self_toTensor_apply, complexLorentzTensor.leftAltLeftUnit_eq_leftBasis_altLeftBasis, complexLorentzTensor.rightAltRightUnit_eq_rightBasis_altRightBasis, Tensorial.toTensor_smul, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, complexLorentzTensor.contrMetric_eq_complexContrBasisFin4, SpaceTime.tensorDeriv_toTensor_basis_repr, complexLorentzTensor.coMetric_symm, complexLorentzTensor.ofRat_basis_repr_apply, complexLorentzTensor.altRightMetric_eq_altRightBasis, complexLorentzTensor.altLeftLeftUnit_eq_basis, PauliMatrix.pauliCoDown_trace_pauliCo, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix, complexLorentzTensor.actionT_altRightRightUnit, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, Tensorial.smul_eq, complexLorentzTensor.actionT_rightAltRightUnit, complexLorentzTensor.actionT_coContrUnit, contrT_metricTensor_metricTensor, Tensor.fromDualMap_apply, realLorentzTensor.contrMetric_eq_fromPairT, complexLorentzTensor.actionT_altLeftLeftUnit, permT_fromPairTContr_metric_metric, complexLorentzTensor.permT_ofRat, complexLorentzTensor.rightMetric_eq_rightBasis, complexLorentzTensor.contrMetric_eq_complexContrBasis, Tensor.prodT_assoc', Tensor.actionT_fromTripleT, complexLorentzTensor.coContrUnit_eq_ofRat, complexLorentzTensor.actionT_rightMetric, Tensor.fromTripleT_apply_basis, Tensor.permT_congr_eq_id', complexLorentzTensor.coMetric_contr_contrMetric, Tensor.fromPairTContr_tmul_tmul, complexLorentzTensor.leftAltLeftUnit_eq_fromPairT, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Tensor.fromPairT_basis_repr, complexLorentzTensor.leftMetric_eq_basis, Tensor.permT_congr_eq_id, Tensor.fromPairT_apply_basis_repr, PauliMatrix.smul_pauliCo, complexLorentzTensor.altRightMetric_eq_ofRat, Tensor.contrT_permT, Tensor.Pure.contrP_symm, complexLorentzTensor.coContrUnit_symm, complexLorentzTensor.contrMetric_eq_fromPairT, Tensor.permT_congr, Lorentz.Vector.tensor_basis_repr_toTensor_apply, PauliMatrix.pauliContrDown_ofRat, Tensor.contrT_equivariant, Tensor.contrT_prodT_snd, F_def, Lorentz.CoVector.basis_eq_map_tensor_basis, Tensor.toField_default, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4, complexLorentzTensor.leftAltLeftUnit_eq_ofRat, complexLorentzTensor.altRightRightUnit_eq_ofRat, Lorentz.CoVector.tensor_basis_map_eq_basis_reindex, complexLorentzTensor.coMetric_eq_ofRat, complexLorentzTensor.leftMetric_eq_leftBasis, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, Tensor.toDualMap_eq_permT_fromDualMap, complexLorentzTensor.basis_eq_ofRat, Tensor.actionT_eq, Tensor.TensorInt.basis_repr_apply, fromPairTContr_metric_metric_eq_permT_unit, complexLorentzTensor.altRightRightUnit_eq_fromPairT, realLorentzTensor.toComplex_eq_sum_basis, Tensor.fromTripleT_tmul, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, complexLorentzTensor.contrCoUnit_eq_ofRat, Tensor.basis_eq_tensorInt, Tensor.toField_equivariant, Tensor.toField_pure, Tensor.fromPairT_comm, complexLorentzTensor.leftMetric_antisymm, complexLorentzTensor.actionT_contrMetric, complexLorentzTensor.altRightMetric_eq_basis, Tensor.instFiniteDimensional, realLorentzTensor.permT_toComplex, Tensor.contrT_basis_repr_apply_eq_sum_fin, realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix, Tensor.fromDualMap_eq_permT_toDualMap, Tensor.actionT_add, complexLorentzTensor.coMetric_eq_basis, Tensor.permT_permT, complexLorentzTensor.rightMetric_eq_ofRat, unitTensor_congr, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, Tensor.Pure.contrP_update_add, Tensor.toDualMap_apply, Tensor.contrT_fromSingleT_fromSingleT, realLorentzTensor.evalT_toComplex, Tensor.actionT_fromPairT, complexLorentzTensor.rightAltRightUnit_eq_ofRat, Lorentz.CoVector.toTensor_symm_basis, complexLorentzTensor.altRightMetric_eq_fromPairT, complexLorentzTensor.altRightRightUnit_eq_altRightBasis_rightBasis, complexLorentzTensor.contrT_ofRat, Tensor.toDualMap_fromDualMap, unitTensor_eq_permT_dual, complexLorentzTensor.actionT_leftMetric, contrT_single_unitTensor, complexLorentzTensor.contrCoUnit_symm, complexLorentzTensor.altRightMetric_contr_rightMetric, realLorentzTensor.contrT_basis_repr_apply_eq_dropPairSection, PauliMatrix.smul_pauliContrDown, Tensor.actionT_zero, realLorentzTensor.toComplex_equivariant, Tensor.toDual_equivariant, complexLorentzTensor.altLeftLeftUnit_eq_altLeftBasis_leftBasis, realLorentzTensor.toComplex_eq_zero_iff, complexLorentzTensor.actionT_coMetric, Tensor.toField_eq_repr, Lorentz.Vector.toTensor_symm_basis, Tensor.basis_apply, Tensor.Pure.toTensor_update_smul, complexLorentzTensor.coContrUnit_eq_fromPairT, PauliMatrix.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Tensorial.smul_toTensor_symm, complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4, Tensor.contrT_pure, Tensor.actionT_neg, realLorentzTensor.coMetric_eq_fromPairT, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, complexLorentzTensor.actionT_leftAltLeftUnit, Tensor.instIsTopologicalAddGroup, Tensor.fromDualMap_toDualMap, Tensor.fromConstPair_whiskerLeft, complexLorentzTensor.contrMetric_eq_basis, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, complexLorentzTensor.contrCoUnit_eq_basis, Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr, unit_fromSingleTContrFromPairT_eq_fromSingleT, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Lorentz.Vector.toTensor_symm_apply, complexLorentzTensor.rightMetric_antisymm, Tensor.toField_basis_default, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, PauliMatrix.toTensor_symm_basis, Tensor.componentMap_ofComponents, Tensor.Pure.prodP_contrP_snd, complexLorentzTensor.contrCoUnit_eq_fromPairT, complexLorentzTensor.altRightMetric_antisymm, complexLorentzTensor.leftMetric_eq_fromPairT, Tensor.fromConstPair_braid, PauliMatrix.toTensor_basis_expand, complexLorentzTensor.rightMetric_eq_fromPairT, complexLorentzTensor.coMetric_eq_complexCoBasisFin4, Tensor.Pure.evalP_update_add, Tensor.prodT_contrT_snd, Tensor.fromSingleT_map, complexLorentzTensor.altLeftMetric_eq_altLeftBasis, Tensor.prodIndexEquiv_symm_pure, Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr_tmul, Tensor.componentMap_pure, complexLorentzTensor.coMetric_eq_complexCoBasis, Tensor.fromTripleT_basis_repr, Tensor.contrT_basis_repr_apply, PauliMatrix.auliContrDown_pauliContr_mul_add, complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis, Lorentz.CoVector.toTensor_symm_apply, complexLorentzTensor.leftMetric_eq_ofRat, contrT_dual_metricTensor_metricTensor, complexLorentzTensor.leftAltLeftUnit_eq_basis, contrT_metricTensor_metricTensor_eq_dual_unit, complexLorentzTensor.actionT_altRightMetric, Tensor.prodT_swap, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Tensorial.toTensor_tprod, Lorentz.CoVector.toTensor_basis_eq_tensor_basis, Tensor.prodT_permT_right, PauliMatrix.toTensor_eq_asConsTensor, complexLorentzTensor.actionT_contrCoUnit, Tensor.prodT_assoc, Tensor.contrT_symm, complexLorentzTensor.rightAltRightUnit_symm, complexLorentzTensor.contrMetric_eq_ofRat, Tensor.ofComponents_componentMap, complexLorentzTensor.prodT_ofRat_ofRat, complexLorentzTensor.coMetric_eq_fromPairT, Tensor.prodT_pure, PauliMatrix.toTensor_eq_ofRat, Tensor.finrank_tensor_eq, Tensor.fromSingleT_eq_pureT, Tensor.fromSingleTContrFromPairT_tmul, PauliMatrix.pauliContr_mul_pauliContrDown_add, Tensor.prodT_permT_left, Tensor.Pure.toTensor_update_add, complexLorentzTensor.altLeftLeftUnit_eq_fromPairT, complexLorentzTensor.altLeftLeftUnit_symm, Tensor.Pure.contrP_update_smul, complexLorentzTensor.leftAltLeftUnit_symm, complexLorentzTensor.altRightRightUnit_eq_basis, Tensor.basis_prod_eq, Tensor.fromSingleT_symm_pure, Lorentz.Vector.toTensor_symm_pure, Tensor.fromPairT_map_right, Lorentz.Vector.tensor_basis_map_eq_basis_reindex, complexLorentzTensor.rightMetric_contr_altRightMetric, Tensor.prodT_equivariant, complexLorentzTensor.altRightRightUnit_symm, PauliMatrix.pauliCo_eq_ofRat, Tensor.permT_pure, realLorentzTensor.contrT_basis_repr_apply_eq_fin, Tensor.prodT_default_right, Tensor.fromPairT_tmul, Tensor.actionT_fromSingleT, Tensor.permT_eq_zero_iff, Tensorial.basis_toTensor_apply, Tensor.prodT_basis, Lorentz.Vector.basis_eq_map_tensor_basis, PauliMatrix.pauliCo_trace_pauliCoDown, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr, complexLorentzTensor.actionT_altLeftMetric, Tensor.fromSingleT_contr_fromPairT_tmul
|
FD 📖 | CompOp | 108 mathmath: Tensor.Pure.componentMap_apply, Tensor.contrT_fromSingleT_fromPairT, Tensor.Pure.μ_toTensor_tmul_toTensor, complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis, Tensor.Pure.evalPCoeff_update_self, unit_app_eq_dual_unit_app, contr_unit, complexLorentzTensor.rightAltRightUnit_eq_fromPairT, castFin0ToField_tprod, FD_map_basis, complexLorentzTensor.basis_downR_eq, complexLorentzTensor.altLeftMetric_eq_fromPairT, Tensor.Pure.congr_mid, Tensor.Pure.evalP_update_smul, Tensor.Pure.map_map_apply, complexLorentzTensor.basis_up_eq, contr_tmul_symm, complexLorentzTensor.leftAltLeftUnit_eq_leftBasis_altLeftBasis, complexLorentzTensor.rightAltRightUnit_eq_rightBasis_altRightBasis, complexLorentzTensor.contrMetric_eq_complexContrBasisFin4, Tensor.Pure.contrPCoeff_update_fst_smul, complexLorentzTensor.altRightMetric_eq_altRightBasis, Tensor.Pure.component_update_add, complexLorentzTensor.basis_contr, Tensor.Pure.toTensor_apply, realLorentzTensor.contrMetric_eq_fromPairT, permT_fromPairTContr_metric_metric, complexLorentzTensor.rightMetric_eq_rightBasis, complexLorentzTensor.contrMetric_eq_complexContrBasis, Tensor.actionT_fromTripleT, Tensor.Pure.prodP_apply_natAdd, complexLorentzTensor.basis_downL_eq, Tensor.fromTripleT_apply_basis, Tensor.fromPairTContr_tmul_tmul, Tensor.Pure.congr_right, complexLorentzTensor.leftAltLeftUnit_eq_fromPairT, complexLorentzTensor.basis_upR_eq, Tensor.fromPairT_basis_repr, Tensor.fromPairT_apply_basis_repr, complexLorentzTensor.contrMetric_eq_fromPairT, F_def, Tensor.toField_default, complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4, Tensor.Pure.component_update_smul, complexLorentzTensor.leftMetric_eq_leftBasis, Tensor.Pure.contrPCoeff_update_snd_add, fromPairTContr_metric_metric_eq_permT_unit, complexLorentzTensor.altRightRightUnit_eq_fromPairT, Tensor.fromTripleT_tmul, Tensor.fromPairT_comm, Tensor.contrT_basis_repr_apply_eq_sum_fin, Tensor.Pure.contrP_update_add, Tensor.contrT_fromSingleT_fromSingleT, contr_metric, Tensor.actionT_fromPairT, complexLorentzTensor.altRightMetric_eq_fromPairT, complexLorentzTensor.altRightRightUnit_eq_altRightBasis_rightBasis, complexLorentzTensor.basis_down_eq, realLorentzTensor.contr_basis, complexLorentzTensor.altLeftLeftUnit_eq_altLeftBasis_leftBasis, Tensor.Pure.toTensor_update_smul, complexLorentzTensor.coContrUnit_eq_fromPairT, Tensor.Pure.prodP_apply_finSumFinEquiv, Tensor.Pure.contrPCoeff_update_fst_add, complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4, realLorentzTensor.coMetric_eq_fromPairT, Tensor.fromConstPair_whiskerLeft, Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr, contr_congr, Tensor.Pure.map_mid_move_left, unit_fromSingleTContrFromPairT_eq_fromSingleT, complexLorentzTensor.contrCoUnit_eq_fromPairT, Tensor.Pure.component_eq_drop, complexLorentzTensor.leftMetric_eq_fromPairT, basis_congr, Tensor.fromConstPair_braid, unit_symm, complexLorentzTensor.rightMetric_eq_fromPairT, complexLorentzTensor.coMetric_eq_complexCoBasisFin4, Tensor.Pure.evalP_update_add, Tensor.fromSingleT_map, complexLorentzTensor.altLeftMetric_eq_altLeftBasis, Tensor.prodIndexEquiv_symm_pure, Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr_tmul, Tensor.componentMap_pure, complexLorentzTensor.coMetric_eq_complexCoBasis, Tensor.fromTripleT_basis_repr, Tensor.Pure.prodP_apply_castAdd, Tensor.contrT_basis_repr_apply, Tensor.Pure.actionP_eq, complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis, basis_congr_repr, Tensor.Pure.contrPCoeff_update_snd_smul, complexLorentzTensor.coMetric_eq_fromPairT, Tensor.fromSingleT_eq_pureT, Tensor.fromSingleTContrFromPairT_tmul, complexLorentzTensor.contr_basis_ratComplexNum, Tensor.Pure.toTensor_update_add, complexLorentzTensor.altLeftLeftUnit_eq_fromPairT, Tensor.Pure.contrP_update_smul, Tensor.fromSingleT_symm_pure, Tensor.fromPairT_map_right, complexLorentzTensor.basis_upL_eq, Tensor.Pure.component_eq, Tensor.prodT_default_right, Tensor.fromPairT_tmul, Tensor.actionT_fromSingleT, Tensor.fromSingleT_contr_fromPairT_tmul
|
F_braided 📖 | CompOp | — |
F_laxBraided 📖 | CompOp | 1 mathmath: Tensor.Pure.μ_toTensor_tmul_toTensor
|
F_monoidal 📖 | CompOp | — |
basis 📖 | CompOp | 21 mathmath: Tensor.Pure.evalPCoeff_update_self, FD_map_basis, complexLorentzTensor.basis_downR_eq, complexLorentzTensor.basis_up_eq, complexLorentzTensor.basis_contr, complexLorentzTensor.basis_downL_eq, Tensor.fromTripleT_apply_basis, complexLorentzTensor.basis_upR_eq, Tensor.fromPairT_basis_repr, Tensor.fromPairT_apply_basis_repr, Tensor.contrT_basis_repr_apply_eq_sum_fin, complexLorentzTensor.basis_down_eq, realLorentzTensor.contr_basis, Tensor.Pure.component_eq_drop, basis_congr, Tensor.fromTripleT_basis_repr, Tensor.contrT_basis_repr_apply, basis_congr_repr, complexLorentzTensor.contr_basis_ratComplexNum, complexLorentzTensor.basis_upL_eq, Tensor.Pure.component_eq
|
castFin0ToField 📖 | CompOp | 1 mathmath: castFin0ToField_tprod
|
castToField 📖 | CompOp | 5 mathmath: complexLorentzTensor.basis_contr, Tensor.contrT_basis_repr_apply_eq_sum_fin, realLorentzTensor.contr_basis, Tensor.contrT_basis_repr_apply, complexLorentzTensor.contr_basis_ratComplexNum
|
contr 📖 | CompOp | 12 mathmath: contr_unit, contr_tmul_symm, complexLorentzTensor.basis_contr, Tensor.fromPairTContr_tmul_tmul, Tensor.contrT_basis_repr_apply_eq_sum_fin, Tensor.contrT_fromSingleT_fromSingleT, contr_metric, realLorentzTensor.contr_basis, contr_congr, Tensor.contrT_basis_repr_apply, Tensor.fromSingleTContrFromPairT_tmul, complexLorentzTensor.contr_basis_ratComplexNum
|
metric 📖 | CompOp | 3 mathmath: permT_fromPairTContr_metric_metric, fromPairTContr_metric_metric_eq_permT_unit, contr_metric
|
numIndices 📖 | CompOp | — |
repDim 📖 | CompOp | 83 mathmath: complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection, complexLorentzTensor.rightMetric_eq_basis, Tensor.permT_basis_repr_symm_apply, complexLorentzTensor.coContrUnit_eq_basis, Tensor.Pure.evalPCoeff_update_self, complexLorentzTensor.altLeftLeftUnit_eq_ofRat, realLorentzTensor.complex_repDim_up, complexLorentzTensor.altLeftMetric_eq_basis, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, Tensor.ComponentIdx.prod_apply_finSumFinEquiv, FD_map_basis, PauliMatrix.pauliCoDown_eq_ofRat, complexLorentzTensor.basis_downR_eq, complexLorentzTensor.altLeftMetric_eq_ofRat, complexLorentzTensor.rightAltRightUnit_eq_basis, complexLorentzTensor.basis_up_eq, repDim_τ, complexLorentzTensor.altLeftLeftUnit_eq_basis, complexLorentzTensor.basis_contr, complexLorentzTensor.permT_ofRat, complexLorentzTensor.coContrUnit_eq_ofRat, complexLorentzTensor.basis_downL_eq, Tensor.fromTripleT_apply_basis, complexLorentzTensor.basis_upR_eq, Tensor.fromPairT_basis_repr, complexLorentzTensor.leftMetric_eq_basis, Tensor.fromPairT_apply_basis_repr, complexLorentzTensor.altRightMetric_eq_ofRat, PauliMatrix.pauliContrDown_ofRat, complexLorentzTensor.leftAltLeftUnit_eq_ofRat, complexLorentzTensor.altRightRightUnit_eq_ofRat, complexLorentzTensor.coMetric_eq_ofRat, realLorentzTensor.repDim_eq_one_plus_dim, complexLorentzTensor.basis_eq_ofRat, realLorentzTensor.toComplex_eq_sum_basis, complexLorentzTensor.contrCoUnit_eq_ofRat, Tensor.basis_eq_tensorInt, complexLorentzTensor.altRightMetric_eq_basis, Tensor.contrT_basis_repr_apply_eq_sum_fin, complexLorentzTensor.coMetric_eq_basis, complexLorentzTensor.rightMetric_eq_ofRat, complexLorentzTensor.rightAltRightUnit_eq_ofRat, complexLorentzTensor.contrT_ofRat, realLorentzTensor.repDim_up, realLorentzTensor.repDim_down, complexLorentzTensor.basis_down_eq, instNeZeroNatRepDim, realLorentzTensor.contr_basis, realLorentzTensor.contrT_basis_repr_apply_eq_dropPairSection, Tensor.toField_eq_repr, PauliMatrix.toTensor_symm_apply, complexLorentzTensor.contrMetric_eq_basis, Tensor.ComponentIdx.DropPairSection.ofFinEquiv_apply_fst, Tensor.ComponentIdx.DropPairSection.ofFinEquiv_apply_snd, complexLorentzTensor.contrCoUnit_eq_basis, Lorentz.Vector.toTensor_symm_apply, Tensor.toField_basis_default, PauliMatrix.toTensor_symm_basis, Tensor.Pure.component_eq_drop, basis_congr, PauliMatrix.toTensor_basis_expand, repDim_neZero, Tensor.ComponentIdx.DropPairSection.ofFin_apply_snd, realLorentzTensor.complex_repDim_down, Tensor.fromTripleT_basis_repr, Tensor.contrT_basis_repr_apply, Tensor.ComponentIdx.DropPairSection.ofFin_apply_fst, Lorentz.CoVector.toTensor_symm_apply, complexLorentzTensor.leftMetric_eq_ofRat, complexLorentzTensor.leftAltLeftUnit_eq_basis, basis_congr_repr, Tensor.ComponentIdx.congr_right, complexLorentzTensor.contrMetric_eq_ofRat, Tensor.Pure.permP_basisVector, PauliMatrix.toTensor_eq_ofRat, Tensor.finrank_tensor_eq, complexLorentzTensor.contr_basis_ratComplexNum, Tensor.Pure.component_basisVector, complexLorentzTensor.altRightRightUnit_eq_basis, complexLorentzTensor.basis_upL_eq, Tensor.Pure.component_eq, PauliMatrix.pauliCo_eq_ofRat, realLorentzTensor.contrT_basis_repr_apply_eq_fin
|
unit 📖 | CompOp | 5 mathmath: unit_app_eq_dual_unit_app, contr_unit, contr_metric, unit_fromSingleTContrFromPairT_eq_fromSingleT, unit_symm
|
τ 📖 | CompOp | 64 mathmath: realLorentzTensor.tau_colorToComplex, complexLorentzTensor.contrMetric_contr_coMetric, PauliMatrix.pauliCo_contr_pauliContr, Tensor.contrT_fromSingleT_fromPairT, dual_unitTensor_eq_permT_unitTensor, contrT_unitTensor_dual_single, complexLorentzTensor.altLeftMetric_contr_leftMetric, unit_app_eq_dual_unit_app, contr_unit, unitTensor_invariant, complexLorentzTensor.leftMetric_contr_altLeftMetric, repDim_τ, contr_tmul_symm, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, PauliMatrix.pauliCoDown_trace_pauliCo, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, complexLorentzTensor.basis_contr, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, contrT_metricTensor_metricTensor, Tensor.fromDualMap_apply, permT_fromPairTContr_metric_metric, complexLorentzTensor.coMetric_contr_contrMetric, Tensor.fromPairTContr_tmul_tmul, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Tensor.toDualMap_eq_permT_fromDualMap, fromPairTContr_metric_metric_eq_permT_unit, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, Tensor.fromDualMap_eq_permT_toDualMap, unitTensor_congr, Tensor.toDualMap_apply, Tensor.contrT_fromSingleT_fromSingleT, contr_metric, Tensor.toDualMap_fromDualMap, unitTensor_eq_permT_dual, contrT_single_unitTensor, realLorentzTensor.contr_basis, complexLorentzTensor.altRightMetric_contr_rightMetric, Tensor.toDual_equivariant, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Tensor.fromDualMap_toDualMap, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr, contr_congr, unit_fromSingleTContrFromPairT_eq_fromSingleT, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, unit_symm, Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr_tmul, realLorentzTensor.τ_down_eq_up, τ_τ_apply, PauliMatrix.auliContrDown_pauliContr_mul_add, contrT_dual_metricTensor_metricTensor, contrT_metricTensor_metricTensor_eq_dual_unit, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, realLorentzTensor.derivative_repr, realLorentzTensor.τ_up_eq_down, Tensor.fromSingleTContrFromPairT_tmul, PauliMatrix.pauliContr_mul_pauliContrDown_add, complexLorentzTensor.contr_basis_ratComplexNum, complexLorentzTensor.rightMetric_contr_altRightMetric, complexLorentzTensor.antiSymm_contr_symm, τ_involution, PauliMatrix.pauliCo_trace_pauliCoDown, Tensor.fromSingleT_contr_fromPairT_tmul
|