Def NormedSpace.fromTangentSpace

Modification history

2026-08-20 12:42
Mathlib/Geometry/Manifold/IsManifold/Basic.lean
chore: fix defeq abuse in the definition of MFDeriv (#42193) …
Modified NormedSpace.fromTangentSpaceView on Github →
2026-03-10 16:35
Mathlib/Geometry/Manifold/IsManifold/Basic.lean
feat: mfderiv_smul (#34263) …
Added NormedSpace.fromTangentSpaceView on Github →