Documentation Verification Report

Elab

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

Statistics

MetricCount
DefinitionsindexExpr, tensorExpr, actionTermMap, addTermMap, contrListAdjust, contrTermMap, elaborateTensorNode, equalTermMap, evalAdjustPos, evalTermMap, getAllIndices, getContrPos, getEvalPos, getIndicesFull, getIndicesLeft, getIndicesLeftEq, getIndicesRight, getIndicesRightEq, getNumIndicesExact, getPermutation, getPermutationTerm, getProdIndices, quot, indexExprIsNum, indexExpr_, indexExpr__1, indexPosEq, indexToDual, indexToIdent, indexToNum, negTermMap, nodeTermMap, prodTermMap, smulTermMap, stringToTerm, syntaxFull, quot, tensorExprSyntax, toPairs, withoutContrEval, «indexExprτ(_)»»), «tensorExpr(_)»»), «tensorExpr-_», «tensorExpr_+_», «tensorExpr_=_», «tensorExpr_|__», «tensorExpr_•ₐ_», «tensorExpr_•ₜ_», «tensorExpr_⊗_»
49
Theorems0
Total49

Lean.Parser.Category

Definitions

NameCategoryTheorems
indexExpr 📖CompOp
tensorExpr 📖CompOp

TensorSpecies.Tensor

Definitions

NameCategoryTheorems
actionTermMap 📖CompOp
addTermMap 📖CompOp
contrListAdjust 📖CompOp
contrTermMap 📖CompOp
elaborateTensorNode 📖CompOp
equalTermMap 📖CompOp
evalAdjustPos 📖CompOp
evalTermMap 📖CompOp
getAllIndices 📖CompOp
getContrPos 📖CompOp
getEvalPos 📖CompOp
getIndicesFull 📖CompOp
getIndicesLeft 📖CompOp
getIndicesLeftEq 📖CompOp
getIndicesRight 📖CompOp
getIndicesRightEq 📖CompOp
getNumIndicesExact 📖CompOp
getPermutation 📖CompOp
getPermutationTerm 📖CompOp
getProdIndices 📖CompOp
indexExprIsNum 📖CompOp
indexExpr_ 📖CompOp
indexExpr__1 📖CompOp
indexPosEq 📖CompOp
indexToDual 📖CompOp
indexToIdent 📖CompOp
indexToNum 📖CompOp
negTermMap 📖CompOp
nodeTermMap 📖CompOp
prodTermMap 📖CompOp
smulTermMap 📖CompOp
stringToTerm 📖CompOp
syntaxFull 📖CompOp
tensorExprSyntax 📖CompOp
toPairs 📖CompOp
withoutContrEval 📖CompOp
«indexExprτ(_)» 📖» "API Documentation")CompOp
«tensorExpr(_)» 📖» "API Documentation")CompOp
«tensorExpr-_» 📖CompOp
«tensorExpr_+_» 📖CompOp
«tensorExpr_=_» 📖CompOp
«tensorExpr_|__» 📖CompOp
«tensorExpr_•ₐ_» 📖CompOp
«tensorExpr_•ₜ_» 📖CompOp
«tensorExpr_⊗_» 📖CompOp

TensorSpecies.Tensor.indexExpr

Definitions

NameCategoryTheorems
quot 📖CompOp

TensorSpecies.Tensor.tensorExpr

Definitions

NameCategoryTheorems
quot 📖CompOp

---

← Back to Index