Basic

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

Statistics

Metric	Count
Definitions Tensor, ComponentIdx, cast, PermCond, inv, toEquiv, toHom, actionP, basisVector, component, componentMap, drop, instSMul, permP, toTensor, update, actionT, basis, componentMap, instTopologicalSpace, ofComponents, permT, toField	23
Theorems congr_right, apply_inv_apply, auto, comp, inv_apply_apply, inv_perserve_color, ofHom, on_id, on_id_symm, preserve_color, symm, actionP_eq, componentMap_apply, component_basisVector, component_eq, component_eq_drop, component_update_add, component_update_smul, congr_mid, congr_right, drop_actionP, map_map_apply, map_mid_move_left, permP_basisVector, permP_congr, permP_id_self, permP_permP, toTensor_apply, toTensor_update_add, toTensor_update_smul, update_drop_self, update_same, update_succAbove_apply, update_succAbove_drop, μ_toTensor_tmul_toTensor, actionT_add, actionT_eq, actionT_neg, actionT_pure, actionT_smul, actionT_zero, basis_apply, basis_repr_pure, componentMap_ofComponents, componentMap_pure, fin_cast_permCond, finrank_tensor_eq, induction_on_basis, induction_on_pure, instFiniteDimensional, instIsTopologicalAddGroup, ofComponents_componentMap, permT_basis_repr_symm_apply, permT_congr, permT_congr_eq_id, permT_congr_eq_id', permT_eq_zero_iff, permT_equivariant, permT_id_self, permT_permT, permT_pure, toField_basis_default, toField_default, toField_eq_repr, toField_equivariant, toField_pure	66
Total	89

TensorSpecies

Definitions

Name	Category	Theorems
Tensor 📖	CompOp	272 math math: 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.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, Tensor.actionT_fromConst, 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, SpaceTime.distTensorDeriv_toTensor_basis_repr, unitTensor_invariant, 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, 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, realLorentzTensor.actionT_contrMetric, 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, metricTensor_invariant, Tensor.basis_eq_tensorInt, Tensor.toField_equivariant, Tensor.toField_pure, Tensor.fromPairT_comm, complexLorentzTensor.leftMetric_antisymm, complexLorentzTensor.actionT_contrMetric, complexLorentzTensor.altRightMetric_eq_basis, realLorentzTensor.actionT_coMetric, 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, Tensor.actionT_fromConstPair, 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.Pure.contrP_equivariant, 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, Tensor.actionT_pure, 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.actionT_fromConstTriple, 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

TensorSpecies.Tensor

Definitions

Name	Category	Theorems
ComponentIdx 📖	CompOp	94 math math: Pure.componentMap_apply, TensorSpecies.Tensorial.basis_map_prod, complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection, ComponentIdx.DropPairSection.ofFin_mem_dropPairEmbSection, complexLorentzTensor.rightMetric_eq_basis, prodT_basis_repr_apply, permT_basis_repr_symm_apply, complexLorentzTensor.coContrUnit_eq_basis, complexLorentzTensor.altLeftLeftUnit_eq_ofRat, Lorentz.CoVector.toTensor_symm_pure, complexLorentzTensor.altLeftMetric_eq_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Lorentz.CoVector.tensor_basis_repr_toTensor_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, SpaceTime.distTensorDeriv_toTensor_basis_repr, PauliMatrix.pauliCoDown_eq_ofRat, complexLorentzTensor.altLeftMetric_eq_ofRat, complexLorentzTensor.rightAltRightUnit_eq_basis, Lorentz.Vector.toTensor_basis_eq_tensor_basis, basis_repr_pure, SpaceTime.tensorDeriv_toTensor_basis_repr, complexLorentzTensor.ofRat_basis_repr_apply, complexLorentzTensor.altLeftLeftUnit_eq_basis, realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix, Pure.prodP_component, complexLorentzTensor.permT_ofRat, complexLorentzTensor.coContrUnit_eq_ofRat, fromTripleT_apply_basis, fromPairT_basis_repr, complexLorentzTensor.leftMetric_eq_basis, fromPairT_apply_basis_repr, complexLorentzTensor.altRightMetric_eq_ofRat, Lorentz.Vector.tensor_basis_repr_toTensor_apply, PauliMatrix.pauliContrDown_ofRat, Lorentz.CoVector.basis_eq_map_tensor_basis, complexLorentzTensor.leftAltLeftUnit_eq_ofRat, complexLorentzTensor.altRightRightUnit_eq_ofRat, Lorentz.CoVector.tensor_basis_map_eq_basis_reindex, complexLorentzTensor.coMetric_eq_ofRat, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, complexLorentzTensor.basis_eq_ofRat, TensorInt.basis_repr_apply, realLorentzTensor.toComplex_eq_sum_basis, complexLorentzTensor.contrCoUnit_eq_ofRat, basis_eq_tensorInt, complexLorentzTensor.altRightMetric_eq_basis, contrT_basis_repr_apply_eq_sum_fin, realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix, complexLorentzTensor.coMetric_eq_basis, complexLorentzTensor.rightMetric_eq_ofRat, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, complexLorentzTensor.rightAltRightUnit_eq_ofRat, Lorentz.CoVector.toTensor_symm_basis, complexLorentzTensor.contrT_ofRat, realLorentzTensor.contrT_basis_repr_apply_eq_dropPairSection, toField_eq_repr, Lorentz.Vector.toTensor_symm_basis, basis_apply, PauliMatrix.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, complexLorentzTensor.contrMetric_eq_basis, ComponentIdx.DropPairSection.ofFinEquiv_apply_fst, ComponentIdx.DropPairSection.ofFinEquiv_apply_snd, complexLorentzTensor.contrCoUnit_eq_basis, ComponentIdx.DropPairSection.mem_self_of_dropPair, Lorentz.Vector.toTensor_symm_apply, toField_basis_default, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, PauliMatrix.toTensor_symm_basis, componentMap_ofComponents, PauliMatrix.toTensor_basis_expand, componentMap_pure, fromTripleT_basis_repr, contrT_basis_repr_apply, Lorentz.CoVector.toTensor_symm_apply, complexLorentzTensor.leftMetric_eq_ofRat, complexLorentzTensor.leftAltLeftUnit_eq_basis, Lorentz.CoVector.toTensor_basis_eq_tensor_basis, complexLorentzTensor.contrMetric_eq_ofRat, ofComponents_componentMap, complexLorentzTensor.prodT_ofRat_ofRat, PauliMatrix.toTensor_eq_ofRat, Pure.component_basisVector, complexLorentzTensor.altRightRightUnit_eq_basis, basis_prod_eq, Lorentz.Vector.toTensor_symm_pure, Lorentz.Vector.tensor_basis_map_eq_basis_reindex, PauliMatrix.pauliCo_eq_ofRat, realLorentzTensor.contrT_basis_repr_apply_eq_fin, ComponentIdx.DropPairSection.mem_iff_apply_dropPairEmb_eq, TensorSpecies.Tensorial.basis_toTensor_apply, prodT_basis, Lorentz.Vector.basis_eq_map_tensor_basis, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr
PermCond 📖	MathDef	62 math math: complexLorentzTensor.contrMetric_contr_coMetric, PauliMatrix.pauliCo_contr_pauliContr, contrT_fromSingleT_fromPairT, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, TensorSpecies.contrT_unitTensor_dual_single, complexLorentzTensor.altLeftMetric_contr_leftMetric, complexLorentzTensor.contrMetric_symm, complexLorentzTensor.altLeftMetric_antisymm, PermCond.ofHom, PermCond.on_id, permT_id_self, TensorSpecies.metricTensor_congr, Pure.dropPairEmb_permCond_prod, complexLorentzTensor.leftMetric_contr_altLeftMetric, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, complexLorentzTensor.coMetric_symm, PauliMatrix.pauliCoDown_trace_pauliCo, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, Pure.prodP_zero_right_permCond, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, fromDualMap_apply, fin_cast_permCond, complexLorentzTensor.coMetric_contr_contrMetric, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Pure.contrP_symm, complexLorentzTensor.coContrUnit_symm, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, toDualMap_eq_permT_fromDualMap, prodAssocMap'_permCond, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, complexLorentzTensor.leftMetric_antisymm, fromDualMap_eq_permT_toDualMap, TensorSpecies.unitTensor_congr, toDualMap_apply, TensorSpecies.contrT_single_unitTensor, complexLorentzTensor.contrCoUnit_symm, complexLorentzTensor.altRightMetric_contr_rightMetric, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Pure.permP_id_self, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, fromPairT_contr_fromPairT_eq_fromPairTContr, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, complexLorentzTensor.rightMetric_antisymm, complexLorentzTensor.altRightMetric_antisymm, prodSwapMap_permCond, fromSingleT_map, fromPairT_contr_fromPairT_eq_fromPairTContr_tmul, PauliMatrix.auliContrDown_pauliContr_mul_add, TensorSpecies.contrT_dual_metricTensor_metricTensor, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, contrT_symm, complexLorentzTensor.rightAltRightUnit_symm, prodAssocMap_permCond, PauliMatrix.pauliContr_mul_pauliContrDown_add, complexLorentzTensor.altLeftLeftUnit_symm, complexLorentzTensor.leftAltLeftUnit_symm, fromPairT_map_right, complexLorentzTensor.rightMetric_contr_altRightMetric, complexLorentzTensor.altRightRightUnit_symm, Pure.dropPair_symm, PauliMatrix.pauliCo_trace_pauliCoDown, fromSingleT_contr_fromPairT_tmul
actionT 📖	CompOp	22 math math: actionT_smul, actionT_fromConst, TensorSpecies.unitTensor_invariant, permT_equivariant, actionT_fromTripleT, contrT_equivariant, realLorentzTensor.actionT_contrMetric, actionT_eq, TensorSpecies.metricTensor_invariant, toField_equivariant, realLorentzTensor.actionT_coMetric, actionT_add, actionT_fromPairT, actionT_zero, toDual_equivariant, actionT_neg, actionT_fromConstPair, Pure.contrP_equivariant, actionT_pure, prodT_equivariant, actionT_fromConstTriple, actionT_fromSingleT
basis 📖	CompOp	61 math math: TensorSpecies.Tensorial.basis_map_prod, complexLorentzTensor.rightMetric_eq_basis, prodT_basis_repr_apply, permT_basis_repr_symm_apply, complexLorentzTensor.coContrUnit_eq_basis, complexLorentzTensor.altLeftMetric_eq_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Lorentz.CoVector.tensor_basis_repr_toTensor_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, SpaceTime.distTensorDeriv_toTensor_basis_repr, complexLorentzTensor.rightAltRightUnit_eq_basis, Lorentz.Vector.toTensor_basis_eq_tensor_basis, basis_repr_pure, SpaceTime.tensorDeriv_toTensor_basis_repr, complexLorentzTensor.ofRat_basis_repr_apply, complexLorentzTensor.altLeftLeftUnit_eq_basis, realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix, fromTripleT_apply_basis, fromPairT_basis_repr, complexLorentzTensor.leftMetric_eq_basis, fromPairT_apply_basis_repr, Lorentz.Vector.tensor_basis_repr_toTensor_apply, Lorentz.CoVector.basis_eq_map_tensor_basis, Lorentz.CoVector.tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, complexLorentzTensor.basis_eq_ofRat, TensorInt.basis_repr_apply, realLorentzTensor.toComplex_eq_sum_basis, basis_eq_tensorInt, complexLorentzTensor.altRightMetric_eq_basis, contrT_basis_repr_apply_eq_sum_fin, realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix, complexLorentzTensor.coMetric_eq_basis, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, Lorentz.CoVector.toTensor_symm_basis, realLorentzTensor.contrT_basis_repr_apply_eq_dropPairSection, toField_eq_repr, Lorentz.Vector.toTensor_symm_basis, basis_apply, PauliMatrix.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, complexLorentzTensor.contrMetric_eq_basis, complexLorentzTensor.contrCoUnit_eq_basis, Lorentz.Vector.toTensor_symm_apply, toField_basis_default, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, PauliMatrix.toTensor_symm_basis, PauliMatrix.toTensor_basis_expand, fromTripleT_basis_repr, contrT_basis_repr_apply, Lorentz.CoVector.toTensor_symm_apply, complexLorentzTensor.leftAltLeftUnit_eq_basis, Lorentz.CoVector.toTensor_basis_eq_tensor_basis, complexLorentzTensor.altRightRightUnit_eq_basis, basis_prod_eq, Lorentz.Vector.tensor_basis_map_eq_basis_reindex, realLorentzTensor.contrT_basis_repr_apply_eq_fin, TensorSpecies.Tensorial.basis_toTensor_apply, prodT_basis, Lorentz.Vector.basis_eq_map_tensor_basis, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr
componentMap 📖	CompOp	3 math math: componentMap_ofComponents, componentMap_pure, ofComponents_componentMap
instTopologicalSpace 📖	CompOp	1 math math: instIsTopologicalAddGroup
ofComponents 📖	CompOp	2 math math: componentMap_ofComponents, ofComponents_componentMap
permT 📖	CompOp	87 math math: complexLorentzTensor.contrMetric_contr_coMetric, PauliMatrix.pauliCo_contr_pauliContr, contrT_fromSingleT_fromPairT, TensorSpecies.dual_unitTensor_eq_permT_unitTensor, permT_basis_repr_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, TensorSpecies.contrT_unitTensor_dual_single, complexLorentzTensor.altLeftMetric_contr_leftMetric, contrT_congr, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, complexLorentzTensor.contrMetric_symm, complexLorentzTensor.altLeftMetric_antisymm, contrT_comm, permT_id_self, TensorSpecies.metricTensor_congr, permT_equivariant, complexLorentzTensor.leftMetric_contr_altLeftMetric, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, complexLorentzTensor.coMetric_symm, PauliMatrix.pauliCoDown_trace_pauliCo, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, TensorSpecies.contrT_metricTensor_metricTensor, fromDualMap_apply, TensorSpecies.permT_fromPairTContr_metric_metric, complexLorentzTensor.permT_ofRat, prodT_assoc', permT_congr_eq_id', complexLorentzTensor.coMetric_contr_contrMetric, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, permT_congr_eq_id, contrT_permT, Pure.contrP_symm, complexLorentzTensor.coContrUnit_symm, permT_congr, contrT_prodT_snd, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, toDualMap_eq_permT_fromDualMap, TensorSpecies.fromPairTContr_metric_metric_eq_permT_unit, fromTripleT_tmul, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, fromPairT_comm, complexLorentzTensor.leftMetric_antisymm, realLorentzTensor.permT_toComplex, fromDualMap_eq_permT_toDualMap, permT_permT, TensorSpecies.unitTensor_congr, toDualMap_apply, TensorSpecies.unitTensor_eq_permT_dual, TensorSpecies.contrT_single_unitTensor, complexLorentzTensor.contrCoUnit_symm, complexLorentzTensor.altRightMetric_contr_rightMetric, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, fromConstPair_whiskerLeft, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, fromPairT_contr_fromPairT_eq_fromPairTContr, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, complexLorentzTensor.rightMetric_antisymm, Pure.prodP_contrP_snd, complexLorentzTensor.altRightMetric_antisymm, fromConstPair_braid, prodT_contrT_snd, fromSingleT_map, fromPairT_contr_fromPairT_eq_fromPairTContr_tmul, PauliMatrix.auliContrDown_pauliContr_mul_add, TensorSpecies.contrT_dual_metricTensor_metricTensor, TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit, prodT_swap, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, prodT_permT_right, prodT_assoc, contrT_symm, complexLorentzTensor.rightAltRightUnit_symm, PauliMatrix.pauliContr_mul_pauliContrDown_add, prodT_permT_left, complexLorentzTensor.altLeftLeftUnit_symm, complexLorentzTensor.leftAltLeftUnit_symm, fromPairT_map_right, complexLorentzTensor.rightMetric_contr_altRightMetric, complexLorentzTensor.altRightRightUnit_symm, permT_pure, prodT_default_right, fromPairT_tmul, permT_eq_zero_iff, PauliMatrix.pauliCo_trace_pauliCoDown, fromSingleT_contr_fromPairT_tmul
toField 📖	CompOp	5 math math: toField_default, toField_equivariant, toField_pure, toField_eq_repr, toField_basis_default

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
actionT_add 📖	mathematical	—	TensorSpecies.Tensor actionT IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	actionT_eq
actionT_eq 📖	mathematical	—	TensorSpecies.Tensor actionT IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	—
actionT_neg 📖	mathematical	—	TensorSpecies.Tensor actionT IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	actionT_eq
actionT_pure 📖	mathematical	—	TensorSpecies.Tensor actionT Pure.toTensor Pure Pure.instSMul	—	actionT_eq Pure.toTensor.eq_1 IndexNotation.OverColor.lift.toRep_ρ_tprod
actionT_smul 📖	mathematical	—	TensorSpecies.Tensor actionT IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	actionT_eq
actionT_zero 📖	mathematical	—	TensorSpecies.Tensor actionT IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	—
basis_apply 📖	mathematical	—	ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis Pure.toTensor Pure.basisVector	—	—
basis_repr_pure 📖	mathematical	—	ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis Pure.toTensor Pure.component	—	componentMap_pure Pure.componentMap_apply
componentMap_ofComponents 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ComponentIdx componentMap ofComponents	—	componentMap_pure Pure.componentMap_apply Pure.component_basisVector
componentMap_pure 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ComponentIdx componentMap Pure.toTensor TensorSpecies.FD Pure.componentMap	—	Pure.componentMap_apply
fin_cast_permCond 📖	mathematical	—	PermCond	—	—
finrank_tensor_eq 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.repDim	—	—
induction_on_basis 📖	—	ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis	—	—	—
induction_on_pure 📖	—	Pure.toTensor TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	—	—
instFiniteDimensional 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	—
instIsTopologicalAddGroup 📖	mathematical	—	TensorSpecies.Tensor instTopologicalSpace IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	—
ofComponents_componentMap 📖	mathematical	—	TensorSpecies.Tensor ComponentIdx IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ofComponents componentMap	—	induction_on_pure componentMap_pure Pure.componentMap_apply Pure.component_eq Pure.toTensor.eq_1
permT_basis_repr_symm_apply 📖	mathematical	PermCond	ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis permT TensorSpecies.repDim PermCond.inv PermCond.inv_perserve_color	—	PermCond.inv_perserve_color induction_on_basis basis_apply permT_pure PermCond.preserve_color Pure.permP_basisVector PermCond.inv_apply_apply PermCond.apply_inv_apply
permT_congr 📖	mathematical	PermCond	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT	—	—
permT_congr_eq_id 📖	mathematical	PermCond	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT	—	permT_id_self
permT_congr_eq_id' 📖	mathematical	PermCond	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT	—	permT_id_self
permT_eq_zero_iff 📖	mathematical	PermCond	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT	—	PermCond.symm PermCond.comp permT_permT permT_congr_eq_id' PermCond.inv_apply_apply
permT_equivariant 📖	mathematical	PermCond	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT actionT	—	—
permT_id_self 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT PermCond	—	induction_on_pure permT_pure Pure.permP_id_self
permT_permT 📖	mathematical	PermCond	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT PermCond.comp	—	PermCond.comp induction_on_basis basis_apply permT_pure PermCond.preserve_color Pure.permP_basisVector permT_congr
permT_pure 📖	mathematical	PermCond	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F permT Pure.toTensor Pure.permP	—	IndexNotation.OverColor.Hom.toEquiv_comp_inv_apply IndexNotation.OverColor.lift.map_tprod
toField_basis_default 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toField ComponentIdx basis TensorSpecies.repDim	—	basis_apply toField_pure
toField_default 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toField Pure.toTensor Pure TensorSpecies.FD	—	—
toField_eq_repr 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toField ComponentIdx basis TensorSpecies.repDim	—	toField_basis_default
toField_equivariant 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toField actionT	—	induction_on_pure actionT_pure toField_pure actionT_smul actionT_add
toField_pure 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toField Pure.toTensor	—	toField_default

TensorSpecies.Tensor.ComponentIdx

Definitions

Name	Category	Theorems
cast 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_right 📖	mathematical	—	TensorSpecies.repDim	—	—

TensorSpecies.Tensor.PermCond

Definitions

Name	Category	Theorems
inv 📖	CompOp	6 math math: apply_inv_apply, TensorSpecies.Tensor.permT_basis_repr_symm_apply, inv_apply_apply, complexLorentzTensor.permT_ofRat, symm, inv_perserve_color
toEquiv 📖	CompOp	—
toHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_inv_apply 📖	mathematical	TensorSpecies.Tensor.PermCond	inv	—	—
auto 📖	—	TensorSpecies.Tensor.PermCond	—	—	—
comp 📖	—	TensorSpecies.Tensor.PermCond	—	—	—
inv_apply_apply 📖	mathematical	TensorSpecies.Tensor.PermCond	inv	—	—
inv_perserve_color 📖	mathematical	TensorSpecies.Tensor.PermCond	inv	—	preserve_color
ofHom 📖	mathematical	—	TensorSpecies.Tensor.PermCond IndexNotation.OverColor.left IndexNotation.OverColor.Hom.toEquiv	—	IndexNotation.OverColor.Hom.toEquiv_symm_apply
on_id 📖	mathematical	—	TensorSpecies.Tensor.PermCond	—	—
on_id_symm 📖	—	TensorSpecies.Tensor.PermCond	—	—	—
preserve_color 📖	—	TensorSpecies.Tensor.PermCond	—	—	—
symm 📖	mathematical	TensorSpecies.Tensor.PermCond	inv	—	inv_apply_apply apply_inv_apply inv_perserve_color

TensorSpecies.Tensor.Pure

Definitions

Name	Category	Theorems
actionP 📖	CompOp	—
basisVector 📖	CompOp	6 math math: prodP_basisVector, TensorSpecies.Tensor.basis_apply, dropPair_basisVector, permP_basisVector, component_basisVector, TensorSpecies.Tensor.prodT_basis
component 📖	CompOp	8 math math: componentMap_apply, TensorSpecies.Tensor.basis_repr_pure, component_update_add, prodP_component, component_update_smul, component_eq_drop, component_basisVector, component_eq
componentMap 📖	CompOp	2 math math: componentMap_apply, TensorSpecies.Tensor.componentMap_pure
drop 📖	CompOp	4 math math: drop_actionP, update_drop_self, component_eq_drop, update_succAbove_drop
instSMul 📖	CompOp	7 math math: drop_actionP, prodP_equivariant, contrP_equivariant, dropPair_equivariant, actionP_eq, TensorSpecies.Tensor.actionT_pure, contrPCoeff_invariant
permP 📖	CompOp	16 math math: prodP_assoc, prodP_permP_left, permP_congr, dropPair_comm, prodP_assoc', prodP_zero_right, permP_permP, prodP_swap, prodP_permP_right, permP_id_self, permP_basisVector, dropPair_permP, TensorSpecies.Tensor.permT_pure, dropPair_symm, contrPCoeff_permP, prodP_dropPair
toTensor 📖	CompOp	22 math math: μ_toTensor_tmul_toTensor, Lorentz.CoVector.toTensor_symm_pure, TensorSpecies.Tensor.basis_repr_pure, toTensor_apply, TensorSpecies.Tensor.toField_default, TensorSpecies.Tensor.toField_pure, TensorSpecies.Tensor.contrT_fromSingleT_fromSingleT, TensorSpecies.Tensor.basis_apply, toTensor_update_smul, TensorSpecies.Tensor.contrT_pure, prodP_contrP_snd, TensorSpecies.Tensor.prodIndexEquiv_symm_pure, TensorSpecies.Tensor.componentMap_pure, TensorSpecies.Tensor.actionT_pure, TensorSpecies.Tensor.prodT_pure, TensorSpecies.Tensor.fromSingleT_eq_pureT, toTensor_update_add, TensorSpecies.Tensor.fromSingleT_symm_pure, Lorentz.Vector.toTensor_symm_pure, TensorSpecies.Tensor.permT_pure, TensorSpecies.Tensor.prodT_default_right, TensorSpecies.Tensor.prodT_basis
update 📖	CompOp	22 math math: evalPCoeff_update_self, update_drop_self, evalP_update_smul, contrPCoeff_update_fst_smul, component_update_add, evalPCoeff_update_succAbove, component_update_smul, dropPair_update_snd, contrPCoeff_update_dropPairEmb, contrPCoeff_update_snd_add, contrP_update_add, update_same, toTensor_update_smul, contrPCoeff_update_fst_add, dropPair_update_dropPairEmb, evalP_update_add, update_succAbove_apply, contrPCoeff_update_snd_smul, toTensor_update_add, contrP_update_smul, dropPair_update_fst, update_succAbove_drop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
actionP_eq 📖	mathematical	—	TensorSpecies.Tensor.Pure instSMul TensorSpecies.FD	—	—
componentMap_apply 📖	mathematical	—	TensorSpecies.FD TensorSpecies.Tensor.ComponentIdx componentMap component	—	—
component_basisVector 📖	mathematical	—	component basisVector TensorSpecies.Tensor.ComponentIdx TensorSpecies.repDim	—	component_eq
component_eq 📖	mathematical	—	component TensorSpecies.repDim TensorSpecies.FD TensorSpecies.basis	—	—
component_eq_drop 📖	mathematical	—	component TensorSpecies.repDim TensorSpecies.FD TensorSpecies.basis drop	—	—
component_update_add 📖	mathematical	—	component update TensorSpecies.FD	—	component_eq_drop update_same update_drop_self
component_update_smul 📖	mathematical	—	component update TensorSpecies.FD	—	component_eq_drop update_same update_drop_self
congr_mid 📖	mathematical	—	TensorSpecies.FD	—	congr_right
congr_right 📖	mathematical	—	TensorSpecies.FD	—	—
drop_actionP 📖	mathematical	—	drop TensorSpecies.Tensor.Pure instSMul	—	drop.eq_1 actionP_eq
map_map_apply 📖	mathematical	—	TensorSpecies.FD	—	—
map_mid_move_left 📖	mathematical	—	TensorSpecies.FD	—	—
permP_basisVector 📖	mathematical	TensorSpecies.Tensor.PermCond	permP basisVector TensorSpecies.repDim	—	TensorSpecies.Tensor.PermCond.preserve_color
permP_congr 📖	mathematical	TensorSpecies.Tensor.PermCond	permP	—	—
permP_id_self 📖	mathematical	—	permP TensorSpecies.Tensor.PermCond	—	—
permP_permP 📖	mathematical	TensorSpecies.Tensor.PermCond	permP TensorSpecies.Tensor.PermCond.comp	—	TensorSpecies.Tensor.PermCond.comp map_map_apply
toTensor_apply 📖	mathematical	—	toTensor TensorSpecies.FD	—	—
toTensor_update_add 📖	mathematical	—	toTensor update TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	—
toTensor_update_smul 📖	mathematical	—	toTensor update TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	—
update_drop_self 📖	mathematical	—	drop update	—	—
update_same 📖	mathematical	—	update	—	—
update_succAbove_apply 📖	mathematical	—	update	—	—
update_succAbove_drop 📖	mathematical	—	drop update	—	—
μ_toTensor_tmul_toTensor 📖	mathematical	—	IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F IndexNotation.OverColor.instMonoidalCategory IndexNotation.OverColor.instBraidedCategory TensorSpecies.F_laxBraided toTensor IndexNotation.OverColor.left TensorSpecies.FD IndexNotation.OverColor.hom	—	IndexNotation.OverColor.lift.μModEquiv.eq_1 toTensor.eq_1 PhysLean.PiTensorProduct.tmulEquiv_tmul_tprod

---

← Back to Index