Documentation Verification Report

Elab

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

Statistics

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

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
evalTermBracketMap 📖CompOp
evalTermMap 📖CompOp
getAllIndices 📖CompOp
getContrPos 📖CompOp
getEvalBracketPos 📖CompOp
getEvalPos 📖CompOp
getIndicesFull 📖CompOp
getIndicesLeft 📖CompOp
getIndicesLeftEq 📖CompOp
getIndicesRight 📖CompOp
getIndicesRightEq 📖CompOp
getNumIndicesExact 📖CompOp
getPermutation 📖CompOp
getPermutationTerm 📖CompOp
getProdIndices 📖CompOp
indexExprIsBracketEval 📖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[_]» 📖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