Notation
📁 Source: Mathlib/Geometry/Manifold/Notation.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsfindModel, findModels, isCLMReduciblyDefeqCoefficients, totalSpaceMk, termCMDiffAt____, termCMDiff____, termMDiffAt__, termMDiff__, «termCMDiffAt[_]____», «termCMDiff[_]____», «termHasMFDerivAt%______», «termHasMFDerivAt[_]______», «termMDiffAt[_]__», «termMDiff[_]__», «termMfderiv%__», «termMfderiv[_]__», «termT%_» | 17 |
| Theorems | 0 |
| Total | 17 |
Manifold
Definitions
| Name | Category | Theorems |
|---|---|---|
termCMDiffAt____ 📖 | CompOp | — |
termCMDiff____ 📖 | CompOp | — |
termMDiffAt__ 📖 | CompOp | — |
termMDiff__ 📖 | CompOp | — |
«termCMDiffAt[_]____» 📖 | CompOp | — |
«termCMDiff[_]____» 📖 | CompOp | — |
«termHasMFDerivAt%______» 📖 | CompOp | — |
«termHasMFDerivAt[_]______» 📖 | CompOp | — |
«termMDiffAt[_]__» 📖 | CompOp | — |
«termMDiff[_]__» 📖 | CompOp | — |
«termMfderiv%__» 📖 | CompOp | — |
«termMfderiv[_]__» 📖 | CompOp | — |
«termT%_» 📖 | CompOp | — |
Manifold.Elab
Definitions
| Name | Category | Theorems |
|---|---|---|
findModel 📖 | CompOp | — |
findModels 📖 | CompOp | — |
isCLMReduciblyDefeqCoefficients 📖 | CompOp | — |
totalSpaceMk 📖 | CompOp | — |
---