Evaluation

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

Statistics

Metric	Count
Definitions evalP, evalPCoeff, evalPMultilinear, evalT	4
Theorems evalPCoeff_update_self, evalPCoeff_update_succAbove, evalP_update_add, evalP_update_smul, evalT_pure	5
Total	9

TensorSpecies.Tensor

Definitions

Name	Category	Theorems
evalT 📖	CompOp	2 math math: realLorentzTensor.evalT_toComplex, evalT_pure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalT_pure 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F evalT Pure.toTensor Pure.evalP	—	—

TensorSpecies.Tensor.Pure

Definitions

Name	Category	Theorems
evalP 📖	CompOp	4 math math: realLorentzTensor.toComplex_evalP_basisVector, evalP_update_smul, TensorSpecies.Tensor.evalT_pure, evalP_update_add
evalPCoeff 📖	CompOp	2 math math: evalPCoeff_update_self, evalPCoeff_update_succAbove
evalPMultilinear 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalPCoeff_update_self 📖	mathematical	—	evalPCoeff update TensorSpecies.repDim TensorSpecies.FD TensorSpecies.basis	—	update_same
evalPCoeff_update_succAbove 📖	mathematical	—	evalPCoeff update	—	update_succAbove_apply
evalP_update_add 📖	mathematical	—	evalP update TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	evalPCoeff_update_self update_drop_self evalPCoeff_update_succAbove update_succAbove_drop toTensor_update_add
evalP_update_smul 📖	mathematical	—	evalP update TensorSpecies.FD TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F	—	evalPCoeff_update_self update_drop_self evalPCoeff_update_succAbove update_succAbove_drop toTensor_update_smul

---

← Back to Index