Basic

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

Statistics

Metric	Count
Definitions realLorentzTensor, Color, instDecidableEqColor, realLorentzTensorSyntax, «termℝT(_,_)»»)	5
Theorems contrT_basis_repr_apply_eq_dropPairSection, contrT_basis_repr_apply_eq_fin, contr_basis, repDim_down, repDim_eq_one_plus_dim, repDim_up, τ_down_eq_up, τ_up_eq_down	8
Total	13

(root)

Definitions

Name	Category	Theorems
realLorentzTensor 📖	CompOp	109 math math: Lorentz.CoVector.smul_eq_sum, realLorentzTensor.prodT_toComplex, realLorentzTensor.tau_colorToComplex, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, Lorentz.CoVector.toTensor_symm_pure, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Lorentz.CoVector.tensor_basis_repr_toTensor_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, Lorentz.CoVector.smul_eq_mulVec, realLorentzTensor.toComplex_injective, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, SpaceTime.distTensorDeriv_toTensor_basis_repr, Lorentz.Vector.smul_zero, Lorentz.Vector.toTensor_basis_eq_tensor_basis, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, SpaceTime.tensorDeriv_toTensor_basis_repr, LorentzGroup.generalizedBoost_apply_expand, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, LorentzGroup.generalizedBoost_apply, Lorentz.CoVector.smul_neg, realLorentzTensor.contrMetric_eq_fromPairT, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Lorentz.Vector.tensor_basis_repr_toTensor_apply, SpaceTime.distTensorDeriv_equivariant, Lorentz.Vector.boost_inr_other_eq, Lorentz.CoVector.basis_eq_map_tensor_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Lorentz.Vector.neg_smul, realLorentzTensor.actionT_contrMetric, Lorentz.CoVector.tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_equivariant, realLorentzTensor.coMetric_eq_fromConstPair, LorentzGroup.genearlizedBoost_apply_basis, realLorentzTensor.repDim_eq_one_plus_dim, SpaceTime.boost_zero_apply_time_space, Lorentz.CoVector.smul_zero, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, Lorentz.CoVector.smul_basis, realLorentzTensor.toComplex_eq_sum_basis, Lorentz.CoVector.actionCLM_apply, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, Electromagnetism.ElectromagneticPotential.isExtrema_lorentzGroup_apply_iff, SpaceTime.tensorDeriv_equivariant, Lorentz.Vector.smul_eq_sum, realLorentzTensor.actionT_coMetric, SpaceTime.deriv_equivariant, realLorentzTensor.permT_toComplex, realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, realLorentzTensor.evalT_toComplex, Lorentz.CoVector.toTensor_symm_basis, Lorentz.Vector.boost_time_eq, SpaceTime.deriv_comp_lorentz_action, Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum, realLorentzTensor.repDim_up, realLorentzTensor.repDim_down, Lorentz.Vector.minkowskiProduct_invariant, Lorentz.Vector.smul_neg, realLorentzTensor.contr_basis, realLorentzTensor.toComplex_equivariant, Lorentz.Vector.causalCharacter_invariant, realLorentzTensor.toComplex_eq_zero_iff, Lorentz.Vector.toTensor_symm_basis, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, realLorentzTensor.coMetric_eq_fromPairT, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, LorentzGroup.generalizedBoost_apply_snd, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Lorentz.Vector.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, Lorentz.Vector.smul_basis, SpaceTime.boost_x_smul, Lorentz.CoVector.smul_add, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, realLorentzTensor.τ_down_eq_up, realLorentzTensor.contrMetric_eq_fromConstPair, LorentzGroup.toVector_mul, Lorentz.Vector.smul_sub, Lorentz.CoVector.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero, Lorentz.CoVector.toTensor_basis_eq_tensor_basis, SpaceTime.schwartzAction_apply, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, realLorentzTensor.τ_up_eq_down, Lorentz.Vector.smul_eq_mulVec, Electromagnetism.ElectromagneticPotential.deriv_equivariant, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ, SpaceTime.lorentzGroup_smul_dist_apply, Lorentz.Vector.actionCLM_apply, Lorentz.Vector.boost_inr_self_eq, Lorentz.Vector.toTensor_symm_pure, Lorentz.CoVector.smul_sub, Lorentz.Vector.tensor_basis_map_eq_basis_reindex, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ, Electromagnetism.ElectromagneticPotential.toFieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.kineticTerm_equivariant, Lorentz.Vector.smul_add, Lorentz.Vector.basis_eq_map_tensor_basis, Lorentz.Vector.boost_toCoord_eq, LorentzGroup.generalizedBoost_apply_fst, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr

realLorentzTensor

Definitions

Name	Category	Theorems
Color 📖	CompData	110 math math: Lorentz.CoVector.smul_eq_sum, prodT_toComplex, tau_colorToComplex, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, Lorentz.CoVector.toTensor_symm_pure, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Lorentz.CoVector.tensor_basis_repr_toTensor_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, Lorentz.CoVector.smul_eq_mulVec, toComplex_injective, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, SpaceTime.distTensorDeriv_toTensor_basis_repr, Lorentz.Vector.smul_zero, Lorentz.Vector.toTensor_basis_eq_tensor_basis, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, SpaceTime.tensorDeriv_toTensor_basis_repr, LorentzGroup.generalizedBoost_apply_expand, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, contrMetric_repr_apply_eq_minkowskiMatrix, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, LorentzGroup.generalizedBoost_apply, Lorentz.CoVector.smul_neg, contrMetric_eq_fromPairT, colorToComplex_append, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Lorentz.Vector.tensor_basis_repr_toTensor_apply, SpaceTime.distTensorDeriv_equivariant, Lorentz.Vector.boost_inr_other_eq, Lorentz.CoVector.basis_eq_map_tensor_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Lorentz.Vector.neg_smul, actionT_contrMetric, Lorentz.CoVector.tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_equivariant, coMetric_eq_fromConstPair, LorentzGroup.genearlizedBoost_apply_basis, repDim_eq_one_plus_dim, SpaceTime.boost_zero_apply_time_space, Lorentz.CoVector.smul_zero, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, Lorentz.CoVector.smul_basis, toComplex_eq_sum_basis, Lorentz.CoVector.actionCLM_apply, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, Electromagnetism.ElectromagneticPotential.isExtrema_lorentzGroup_apply_iff, SpaceTime.tensorDeriv_equivariant, Lorentz.Vector.smul_eq_sum, actionT_coMetric, SpaceTime.deriv_equivariant, coMetric_repr_apply_eq_minkowskiMatrix, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, evalT_toComplex, Lorentz.CoVector.toTensor_symm_basis, Lorentz.Vector.boost_time_eq, SpaceTime.deriv_comp_lorentz_action, Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum, repDim_up, repDim_down, Lorentz.Vector.minkowskiProduct_invariant, Lorentz.Vector.smul_neg, contr_basis, toComplex_equivariant, Lorentz.Vector.causalCharacter_invariant, toComplex_eq_zero_iff, Lorentz.Vector.toTensor_symm_basis, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, coMetric_eq_fromPairT, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.isExterma_equivariant, LorentzGroup.generalizedBoost_apply_snd, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Lorentz.Vector.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, Lorentz.Vector.smul_basis, SpaceTime.boost_x_smul, Lorentz.CoVector.smul_add, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, τ_down_eq_up, contrMetric_eq_fromConstPair, LorentzGroup.toVector_mul, Lorentz.Vector.smul_sub, Lorentz.CoVector.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero, Lorentz.CoVector.toTensor_basis_eq_tensor_basis, SpaceTime.schwartzAction_apply, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, τ_up_eq_down, Lorentz.Vector.smul_eq_mulVec, Electromagnetism.ElectromagneticPotential.deriv_equivariant, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ, SpaceTime.lorentzGroup_smul_dist_apply, Lorentz.Vector.actionCLM_apply, Lorentz.Vector.boost_inr_self_eq, Lorentz.Vector.toTensor_symm_pure, Lorentz.CoVector.smul_sub, Lorentz.Vector.tensor_basis_map_eq_basis_reindex, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ, Electromagnetism.ElectromagneticPotential.toFieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.kineticTerm_equivariant, Lorentz.Vector.smul_add, Lorentz.Vector.basis_eq_map_tensor_basis, Lorentz.Vector.boost_toCoord_eq, LorentzGroup.generalizedBoost_apply_fst, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr
instDecidableEqColor 📖	CompOp	11 math math: Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add
realLorentzTensorSyntax 📖	CompOp	—
«termℝT(_,_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contrT_basis_repr_apply_eq_dropPairSection 📖	mathematical	TensorSpecies.τ Color LorentzGroup lorentzGroupIsGroup realLorentzTensor	TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.Pure.dropPairEmb TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis TensorSpecies.Tensor.contrT TensorSpecies.Tensor.ComponentIdx.DropPairSection TensorSpecies.repDim	—	TensorSpecies.Tensor.contrT_basis_repr_apply contr_basis
contrT_basis_repr_apply_eq_fin 📖	mathematical	TensorSpecies.τ Color LorentzGroup lorentzGroupIsGroup realLorentzTensor	TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.Pure.dropPairEmb TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis TensorSpecies.Tensor.contrT TensorSpecies.Tensor.ComponentIdx.DropPairSection TensorSpecies.repDim TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv repDim_eq_one_plus_dim	—	repDim_eq_one_plus_dim TensorSpecies.Tensor.contrT_basis_repr_apply_eq_sum_fin contr_basis
contr_basis 📖	mathematical	—	TensorSpecies.castToField LorentzGroup Color lorentzGroupIsGroup realLorentzTensor IndexNotation.OverColor.Discrete.pairτ TensorSpecies.FD TensorSpecies.τ TensorSpecies.contr TensorSpecies.repDim TensorSpecies.basis	—	Lorentz.contrCoContract_hom_tmul Lorentz.contrBasis_toFin1dℝ Lorentz.coBasisFin_toFin1dℝ Lorentz.coContrContract_hom_tmul Lorentz.contrBasisFin_toFin1dℝ
repDim_down 📖	mathematical	—	TensorSpecies.repDim Color LorentzGroup lorentzGroupIsGroup realLorentzTensor Color.down	—	—
repDim_eq_one_plus_dim 📖	mathematical	—	TensorSpecies.repDim Color LorentzGroup lorentzGroupIsGroup realLorentzTensor	—	—
repDim_up 📖	mathematical	—	TensorSpecies.repDim Color LorentzGroup lorentzGroupIsGroup realLorentzTensor Color.up	—	—
τ_down_eq_up 📖	mathematical	—	TensorSpecies.τ Color LorentzGroup lorentzGroupIsGroup realLorentzTensor Color.down Color.up	—	—
τ_up_eq_down 📖	mathematical	—	TensorSpecies.τ Color LorentzGroup lorentzGroupIsGroup realLorentzTensor Color.up Color.down	—	—

---

← Back to Index