Documentation Verification Report

Tensorial

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

Statistics

Metric	Count
Definitions `Tensorial`, `actionCLM`, `distribMulAction`, `mulAction`, `numIndices`, `prod`, `self`, `smulAction`, `smulLinearMap`, `toTensor`, `toTensorCLM`	11
Theorems `actionCLM_apply`, `basis_map_prod`, `basis_toTensor_apply`, `instFiniteDimensional`, `instSMulCommClass`, `self_toTensor_apply`, `smulLinearMap_apply`, `smul_eq`, `smul_prod`, `smul_toTensor_symm`, `toTensor_smul`, `toTensor_tprod`	12
Total	23

TensorSpecies

Definitions

Name	Category	Theorems
`Tensorial` 📖	CompData	—

TensorSpecies.Tensorial

Definitions

Name	Category	Theorems
`actionCLM` 📖	CompOp	1 math math: `actionCLM_apply`
`distribMulAction` 📖	CompOp	—
`mulAction` 📖	CompOp	—
`numIndices` 📖	CompOp	—
`prod` 📖	CompOp	29 math math: `basis_map_prod`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis`, `Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr`, `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`, `Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor`, `SpaceTime.distTensorDeriv_equivariant`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add`, `Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply`, `Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength`, `SpaceTime.tensorDeriv_equivariant`, `Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr`, `smul_prod`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv`, `Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add`, `toTensor_tprod`, `Electromagnetism.DistElectromagneticPotential.deriv_equivariant`, `Electromagnetism.ElectromagneticPotential.deriv_equivariant`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_equivariant`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr`
`self` 📖	CompOp	48 math math: `complexLorentzTensor.contrMetric_contr_coMetric`, `PauliMatrix.pauliCo_contr_pauliContr`, `PauliMatrix.smul_pauliCoDown`, `complexLorentzTensor.altLeftMetric_contr_leftMetric`, `complexLorentzTensor.contrMetric_symm`, `complexLorentzTensor.altLeftMetric_antisymm`, `PauliMatrix.toTensor_smul_eq_self`, `complexLorentzTensor.leftMetric_contr_altLeftMetric`, `self_toTensor_apply`, `toTensor_smul`, `complexLorentzTensor.coMetric_symm`, `PauliMatrix.pauliCoDown_trace_pauliCo`, `complexLorentzTensor.actionT_altRightRightUnit`, `smul_eq`, `complexLorentzTensor.actionT_rightAltRightUnit`, `complexLorentzTensor.actionT_coContrUnit`, `complexLorentzTensor.actionT_altLeftLeftUnit`, `complexLorentzTensor.actionT_rightMetric`, `complexLorentzTensor.coMetric_contr_contrMetric`, `PauliMatrix.smul_pauliCo`, `complexLorentzTensor.coContrUnit_symm`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add`, `Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength`, `complexLorentzTensor.leftMetric_antisymm`, `complexLorentzTensor.actionT_contrMetric`, `complexLorentzTensor.actionT_leftMetric`, `complexLorentzTensor.contrCoUnit_symm`, `complexLorentzTensor.altRightMetric_contr_rightMetric`, `PauliMatrix.smul_pauliContrDown`, `realLorentzTensor.toComplex_equivariant`, `complexLorentzTensor.actionT_coMetric`, `smul_toTensor_symm`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux`, `complexLorentzTensor.actionT_leftAltLeftUnit`, `complexLorentzTensor.rightMetric_antisymm`, `complexLorentzTensor.altRightMetric_antisymm`, `PauliMatrix.auliContrDown_pauliContr_mul_add`, `complexLorentzTensor.actionT_altRightMetric`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add`, `complexLorentzTensor.actionT_contrCoUnit`, `complexLorentzTensor.rightAltRightUnit_symm`, `PauliMatrix.pauliContr_mul_pauliContrDown_add`, `complexLorentzTensor.altLeftLeftUnit_symm`, `complexLorentzTensor.leftAltLeftUnit_symm`, `complexLorentzTensor.rightMetric_contr_altRightMetric`, `complexLorentzTensor.altRightRightUnit_symm`, `PauliMatrix.pauliCo_trace_pauliCoDown`, `complexLorentzTensor.actionT_altLeftMetric`
`smulAction` 📖	CompOp	73 math math: `Lorentz.CoVector.smul_eq_sum`, `PauliMatrix.smul_pauliCoDown`, `Lorentz.CoVector.smul_eq_mulVec`, `PauliMatrix.toTensor_smul_eq_self`, `Lorentz.Vector.smul_zero`, `actionCLM_apply`, `toTensor_smul`, `LorentzGroup.generalizedBoost_apply_expand`, `complexLorentzTensor.actionT_altRightRightUnit`, `smul_eq`, `LorentzGroup.generalizedBoost_apply`, `Lorentz.CoVector.smul_neg`, `complexLorentzTensor.actionT_rightAltRightUnit`, `complexLorentzTensor.actionT_coContrUnit`, `complexLorentzTensor.actionT_altLeftLeftUnit`, `complexLorentzTensor.actionT_rightMetric`, `PauliMatrix.smul_pauliCo`, `Lorentz.Vector.boost_inr_other_eq`, `Lorentz.Vector.neg_smul`, `Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_equivariant`, `LorentzGroup.genearlizedBoost_apply_basis`, `SpaceTime.boost_zero_apply_time_space`, `Lorentz.CoVector.smul_zero`, `LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct`, `Lorentz.CoVector.smul_basis`, `Lorentz.CoVector.actionCLM_apply`, `Electromagnetism.ElectromagneticPotential.isExtrema_lorentzGroup_apply_iff`, `SpaceTime.tensorDeriv_equivariant`, `Lorentz.Vector.smul_eq_sum`, `instSMulCommClass`, `complexLorentzTensor.actionT_contrMetric`, `SpaceTime.deriv_equivariant`, `Lorentz.Vector.boost_time_eq`, `SpaceTime.deriv_comp_lorentz_action`, `Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum`, `complexLorentzTensor.actionT_leftMetric`, `Lorentz.Vector.minkowskiProduct_invariant`, `Lorentz.Vector.smul_neg`, `smul_prod`, `PauliMatrix.smul_pauliContrDown`, `realLorentzTensor.toComplex_equivariant`, `Lorentz.Vector.causalCharacter_invariant`, `complexLorentzTensor.actionT_coMetric`, `smul_toTensor_symm`, `complexLorentzTensor.actionT_leftAltLeftUnit`, `LorentzGroup.generalizedBoost_apply_snd`, `Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ`, `PauliMatrix.smul_eq_self`, `Lorentz.Vector.smul_basis`, `SpaceTime.boost_x_smul`, `Lorentz.CoVector.smul_add`, `LorentzGroup.generalizedBoost_apply_mul_one_plus_contr`, `smulLinearMap_apply`, `LorentzGroup.toVector_mul`, `Lorentz.Vector.smul_sub`, `complexLorentzTensor.actionT_altRightMetric`, `Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero`, `SpaceTime.schwartzAction_apply`, `complexLorentzTensor.actionT_contrCoUnit`, `Lorentz.Vector.smul_eq_mulVec`, `Electromagnetism.ElectromagneticPotential.deriv_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.CoVector.smul_sub`, `Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_equivariant`, `Electromagnetism.ElectromagneticPotential.kineticTerm_equivariant`, `Lorentz.Vector.smul_add`, `Lorentz.Vector.boost_toCoord_eq`, `LorentzGroup.generalizedBoost_apply_fst`, `complexLorentzTensor.actionT_altLeftMetric`
`smulLinearMap` 📖	CompOp	1 math math: `smulLinearMap_apply`
`toTensor` 📖	CompOp	72 math math: `basis_map_prod`, `complexLorentzTensor.contrMetric_contr_coMetric`, `PauliMatrix.pauliCo_contr_pauliContr`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric`, `complexLorentzTensor.altLeftMetric_contr_leftMetric`, `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`, `Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor`, `complexLorentzTensor.contrMetric_symm`, `complexLorentzTensor.altLeftMetric_antisymm`, `SpaceTime.distTensorDeriv_toTensor_basis_repr`, `PauliMatrix.toTensor_smul_eq_self`, `Lorentz.Vector.toTensor_basis_eq_tensor_basis`, `complexLorentzTensor.leftMetric_contr_altLeftMetric`, `self_toTensor_apply`, `toTensor_smul`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor`, `SpaceTime.tensorDeriv_toTensor_basis_repr`, `complexLorentzTensor.coMetric_symm`, `PauliMatrix.pauliCoDown_trace_pauliCo`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv`, `smul_eq`, `complexLorentzTensor.coMetric_contr_contrMetric`, `Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor`, `complexLorentzTensor.coContrUnit_symm`, `Lorentz.Vector.tensor_basis_repr_toTensor_apply`, `Lorentz.CoVector.basis_eq_map_tensor_basis`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add`, `Lorentz.CoVector.tensor_basis_map_eq_basis_reindex`, `Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply`, `Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength`, `complexLorentzTensor.leftMetric_antisymm`, `Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr`, `Lorentz.CoVector.toTensor_symm_basis`, `complexLorentzTensor.contrCoUnit_symm`, `complexLorentzTensor.altRightMetric_contr_rightMetric`, `Lorentz.Vector.toTensor_symm_basis`, `PauliMatrix.toTensor_symm_apply`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor`, `smul_toTensor_symm`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv`, `Lorentz.Vector.toTensor_symm_apply`, `complexLorentzTensor.rightMetric_antisymm`, `Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply`, `PauliMatrix.toTensor_symm_basis`, `complexLorentzTensor.altRightMetric_antisymm`, `PauliMatrix.toTensor_basis_expand`, `PauliMatrix.auliContrDown_pauliContr_mul_add`, `Lorentz.CoVector.toTensor_symm_apply`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add`, `toTensor_tprod`, `Lorentz.CoVector.toTensor_basis_eq_tensor_basis`, `PauliMatrix.toTensor_eq_asConsTensor`, `complexLorentzTensor.rightAltRightUnit_symm`, `PauliMatrix.toTensor_eq_ofRat`, `PauliMatrix.pauliContr_mul_pauliContrDown_add`, `complexLorentzTensor.altLeftLeftUnit_symm`, `complexLorentzTensor.leftAltLeftUnit_symm`, `Lorentz.Vector.toTensor_symm_pure`, `Lorentz.Vector.tensor_basis_map_eq_basis_reindex`, `complexLorentzTensor.rightMetric_contr_altRightMetric`, `complexLorentzTensor.altRightRightUnit_symm`, `basis_toTensor_apply`, `Lorentz.Vector.basis_eq_map_tensor_basis`, `PauliMatrix.pauliCo_trace_pauliCoDown`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr`
`toTensorCLM` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`actionCLM_apply` 📖	mathematical	—	`actionCLM` `smulAction`	—	—
`basis_map_prod` 📖	mathematical	—	`TensorSpecies.Tensor.ComponentIdx` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.basis` `toTensor` `prod` `TensorSpecies.Tensor.ComponentIdx.prodEquiv`	—	`TensorSpecies.Tensor.basis_prod_eq` `toTensor_tprod`
`basis_toTensor_apply` 📖	mathematical	—	`TensorSpecies.Tensor` `TensorSpecies.Tensor.ComponentIdx` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.basis` `toTensor`	—	—
`instFiniteDimensional` 📖	—	—	—	—	`TensorSpecies.Tensor.instFiniteDimensional`
`instSMulCommClass` 📖	mathematical	—	`smulAction`	—	`toTensor_smul` `TensorSpecies.Tensor.actionT_smul`
`self_toTensor_apply` 📖	mathematical	—	`TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toTensor` `self`	—	`toTensor.eq_1`
`smulLinearMap_apply` 📖	mathematical	—	`smulLinearMap` `smulAction`	—	—
`smul_eq` 📖	mathematical	—	`smulAction` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toTensor` `self`	—	`toTensor.eq_1`
`smul_prod` 📖	mathematical	—	`smulAction` `prod`	—	`toTensor_smul` `toTensor_tprod` `TensorSpecies.Tensor.prodT_equivariant`
`smul_toTensor_symm` 📖	mathematical	—	`smulAction` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toTensor` `self`	—	`smul_eq`
`toTensor_smul` 📖	mathematical	—	`TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toTensor` `smulAction` `self`	—	`smul_eq`
`toTensor_tprod` 📖	mathematical	—	`TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toTensor` `prod` `TensorSpecies.Tensor.prodT`	—	—

---

← Back to Index