Basic

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

Statistics

Metric	Count
Definitions CoVector, actionCLM, basis, equivEuclid, indexEquiv, innerProductSpace, instAddCommGroup, instAddCommMonoid, instChartedSpace, instCoeFunForallSumFinOfNatNatReal, instInnerReal, instModuleReal, instNorm, isNormedAddCommGroup, isNormedSpace, tensorial	16
Theorems actionCLM_apply, apply_add, apply_smul, apply_sub, basis_apply, basis_eq_map_tensor_basis, basis_repr_apply, inner_eq_equivEuclid, instFiniteDimensionalReal, map_apply_eq_basis_mulVec, neg_apply, norm_eq_equivEuclid, smul_add, smul_basis, smul_eq_mulVec, smul_eq_sum, smul_neg, smul_sub, smul_zero, tensor_basis_map_eq_basis_reindex, tensor_basis_repr_toTensor_apply, toTensor_basis_eq_tensor_basis, toTensor_symm_apply, toTensor_symm_basis, toTensor_symm_pure, zero_apply	26
Total	42

Lorentz

Definitions

Name	Category	Theorems
CoVector 📖	CompOp	52 math math: CoVector.smul_eq_sum, CoVector.apply_add, CoVector.toTensor_symm_pure, CoVector.tensor_basis_repr_toTensor_apply, CoVector.smul_eq_mulVec, SpaceTime.distTensorDeriv_toTensor_basis_repr, CoVector.basis_repr_apply, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, SpaceTime.tensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, CoVector.smul_neg, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, SpaceTime.distTensorDeriv_equivariant, CoVector.basis_eq_map_tensor_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, CoVector.tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, CoVector.smul_zero, CoVector.smul_basis, CoVector.basis_apply, CoVector.neg_apply, CoVector.actionCLM_apply, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, SpaceTime.tensorDeriv_equivariant, CoVector.toTensor_symm_basis, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, CoVector.zero_apply, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, CoVector.smul_add, CoVector.inner_eq_equivEuclid, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq, CoVector.instFiniteDimensionalReal, CoVector.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, CoVector.apply_sub, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, CoVector.toTensor_basis_eq_tensor_basis, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, CoVector.apply_smul, CoVector.map_apply_eq_basis_mulVec, Electromagnetism.ElectromagneticPotential.deriv_equivariant, CoVector.smul_sub, CoVector.norm_eq_equivEuclid, SpaceTime.distTensorDeriv_apply

Lorentz.CoVector

Definitions

Name	Category	Theorems
actionCLM 📖	CompOp	1 math math: actionCLM_apply
basis 📖	CompOp	16 math math: basis_repr_apply, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, basis_eq_map_tensor_basis, tensor_basis_map_eq_basis_reindex, smul_basis, basis_apply, toTensor_symm_basis, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, toTensor_basis_eq_tensor_basis, map_apply_eq_basis_mulVec, SpaceTime.distTensorDeriv_apply
equivEuclid 📖	CompOp	2 math math: inner_eq_equivEuclid, norm_eq_equivEuclid
indexEquiv 📖	CompOp	9 math math: toTensor_symm_pure, tensor_basis_repr_toTensor_apply, SpaceTime.distTensorDeriv_toTensor_basis_repr, SpaceTime.tensorDeriv_toTensor_basis_repr, basis_eq_map_tensor_basis, tensor_basis_map_eq_basis_reindex, toTensor_symm_basis, toTensor_symm_apply, toTensor_basis_eq_tensor_basis
innerProductSpace 📖	CompOp	12 math math: SpaceTime.distTensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, SpaceTime.distTensorDeriv_equivariant, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, SpaceTime.distTensorDeriv_apply
instAddCommGroup 📖	CompOp	5 math math: smul_neg, smul_zero, neg_apply, zero_apply, instFiniteDimensionalReal
instAddCommMonoid 📖	CompOp	48 math math: smul_eq_sum, apply_add, toTensor_symm_pure, tensor_basis_repr_toTensor_apply, smul_eq_mulVec, SpaceTime.distTensorDeriv_toTensor_basis_repr, basis_repr_apply, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, SpaceTime.tensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, smul_neg, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, SpaceTime.distTensorDeriv_equivariant, basis_eq_map_tensor_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, smul_zero, smul_basis, basis_apply, actionCLM_apply, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, SpaceTime.tensorDeriv_equivariant, toTensor_symm_basis, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, smul_add, inner_eq_equivEuclid, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq, toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, toTensor_basis_eq_tensor_basis, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, apply_smul, map_apply_eq_basis_mulVec, Electromagnetism.ElectromagneticPotential.deriv_equivariant, smul_sub, norm_eq_equivEuclid, SpaceTime.distTensorDeriv_apply
instChartedSpace 📖	CompOp	—
instCoeFunForallSumFinOfNatNatReal 📖	CompOp	—
instInnerReal 📖	CompOp	1 math math: inner_eq_equivEuclid
instModuleReal 📖	CompOp	48 math math: smul_eq_sum, toTensor_symm_pure, tensor_basis_repr_toTensor_apply, smul_eq_mulVec, SpaceTime.distTensorDeriv_toTensor_basis_repr, basis_repr_apply, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, SpaceTime.tensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, smul_neg, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, SpaceTime.distTensorDeriv_equivariant, basis_eq_map_tensor_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, smul_zero, smul_basis, basis_apply, actionCLM_apply, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, SpaceTime.tensorDeriv_equivariant, toTensor_symm_basis, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, smul_add, inner_eq_equivEuclid, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq, instFiniteDimensionalReal, toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, toTensor_basis_eq_tensor_basis, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, apply_smul, map_apply_eq_basis_mulVec, Electromagnetism.ElectromagneticPotential.deriv_equivariant, smul_sub, norm_eq_equivEuclid, SpaceTime.distTensorDeriv_apply
instNorm 📖	CompOp	1 math math: norm_eq_equivEuclid
isNormedAddCommGroup 📖	CompOp	17 math math: SpaceTime.distTensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, SpaceTime.distTensorDeriv_equivariant, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, smul_basis, actionCLM_apply, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, apply_sub, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, apply_smul, smul_sub, SpaceTime.distTensorDeriv_apply
isNormedSpace 📖	CompOp	—
tensorial 📖	CompOp	33 math math: smul_eq_sum, toTensor_symm_pure, tensor_basis_repr_toTensor_apply, smul_eq_mulVec, SpaceTime.distTensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, SpaceTime.tensorDeriv_toTensor_basis_repr, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, smul_neg, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, SpaceTime.distTensorDeriv_equivariant, basis_eq_map_tensor_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, smul_zero, smul_basis, actionCLM_apply, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, SpaceTime.tensorDeriv_equivariant, toTensor_symm_basis, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, smul_add, toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, toTensor_basis_eq_tensor_basis, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, Electromagnetism.ElectromagneticPotential.deriv_equivariant, smul_sub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
actionCLM_apply 📖	mathematical	—	Lorentz.CoVector isNormedAddCommGroup instAddCommMonoid instModuleReal actionCLM LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down tensorial	—	—
apply_add 📖	mathematical	—	Lorentz.CoVector instAddCommMonoid	—	—
apply_smul 📖	mathematical	—	Lorentz.CoVector isNormedAddCommGroup instAddCommMonoid instModuleReal	—	—
apply_sub 📖	mathematical	—	Lorentz.CoVector isNormedAddCommGroup	—	—
basis_apply 📖	mathematical	—	Lorentz.CoVector instAddCommMonoid instModuleReal basis	—	—
basis_eq_map_tensor_basis 📖	mathematical	—	basis TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down Lorentz.CoVector instAddCommMonoid instModuleReal TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis TensorSpecies.Tensorial.toTensor tensorial indexEquiv	—	toTensor_symm_basis
basis_repr_apply 📖	mathematical	—	Lorentz.CoVector instAddCommMonoid instModuleReal basis	—	—
inner_eq_equivEuclid 📖	mathematical	—	Lorentz.CoVector instInnerReal instAddCommMonoid instModuleReal equivEuclid	—	—
instFiniteDimensionalReal 📖	mathematical	—	Lorentz.CoVector instAddCommGroup instModuleReal	—	—
map_apply_eq_basis_mulVec 📖	mathematical	—	Lorentz.CoVector instAddCommMonoid instModuleReal basis	—	—
neg_apply 📖	mathematical	—	Lorentz.CoVector instAddCommGroup	—	—
norm_eq_equivEuclid 📖	mathematical	—	Lorentz.CoVector instNorm instAddCommMonoid instModuleReal equivEuclid	—	—
smul_add 📖	mathematical	—	LorentzGroup Lorentz.CoVector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down instAddCommMonoid instModuleReal tensorial	—	—
smul_basis 📖	mathematical	—	LorentzGroup Lorentz.CoVector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down instAddCommMonoid instModuleReal tensorial basis isNormedAddCommGroup	—	smul_eq_sum basis_apply
smul_eq_mulVec 📖	mathematical	—	LorentzGroup Lorentz.CoVector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down instAddCommMonoid instModuleReal tensorial LorentzGroup.transpose	—	smul_eq_sum
smul_eq_sum 📖	mathematical	—	LorentzGroup Lorentz.CoVector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down instAddCommMonoid instModuleReal tensorial	—	TensorSpecies.Tensorial.smul_toTensor_symm TensorSpecies.Tensor.induction_on_pure TensorSpecies.Tensor.actionT_pure toTensor_symm_pure Lorentz.coBasisFin_repr_apply Lorentz.CoMod.mulVec_val TensorSpecies.Tensor.actionT_smul TensorSpecies.Tensor.actionT_add
smul_neg 📖	mathematical	—	LorentzGroup Lorentz.CoVector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down instAddCommMonoid instModuleReal tensorial instAddCommGroup	—	smul_eq_mulVec
smul_sub 📖	mathematical	—	LorentzGroup Lorentz.CoVector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down instAddCommMonoid instModuleReal tensorial isNormedAddCommGroup	—	smul_eq_mulVec
smul_zero 📖	mathematical	—	LorentzGroup Lorentz.CoVector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down instAddCommMonoid instModuleReal tensorial instAddCommGroup	—	smul_eq_mulVec
tensor_basis_map_eq_basis_reindex 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down TensorSpecies.Tensor Lorentz.CoVector IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instAddCommMonoid instModuleReal TensorSpecies.Tensor.basis TensorSpecies.Tensorial.toTensor tensorial basis indexEquiv	—	basis_eq_map_tensor_basis
tensor_basis_repr_toTensor_apply 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis Lorentz.CoVector instAddCommMonoid instModuleReal TensorSpecies.Tensorial.toTensor tensorial indexEquiv	—	TensorSpecies.Tensor.induction_on_pure TensorSpecies.Tensor.basis_repr_pure toTensor_symm_pure
toTensor_basis_eq_tensor_basis 📖	mathematical	—	Lorentz.CoVector TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down instAddCommMonoid IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instModuleReal TensorSpecies.Tensorial.toTensor tensorial basis TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis indexEquiv	—	toTensor_symm_basis
toTensor_symm_apply 📖	mathematical	—	TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down Lorentz.CoVector IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instAddCommMonoid instModuleReal TensorSpecies.Tensorial.toTensor tensorial TensorSpecies.Tensor.ComponentIdx indexEquiv TensorSpecies.repDim TensorSpecies.Tensor.basis	—	—
toTensor_symm_basis 📖	mathematical	—	TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down Lorentz.CoVector IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instAddCommMonoid instModuleReal TensorSpecies.Tensorial.toTensor tensorial TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis indexEquiv basis	—	TensorSpecies.Tensor.basis_apply toTensor_symm_pure basis_apply
toTensor_symm_pure 📖	mathematical	—	TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down Lorentz.CoVector IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instAddCommMonoid instModuleReal TensorSpecies.Tensorial.toTensor tensorial TensorSpecies.Tensor.Pure.toTensor Lorentz.Co Lorentz.coBasisFin TensorSpecies.Tensor.ComponentIdx indexEquiv	—	toTensor_symm_apply TensorSpecies.Tensor.basis_repr_pure
zero_apply 📖	mathematical	—	Lorentz.CoVector instAddCommGroup	—	—

---

← Back to Index