Def NormedSpace.fromTangentSpace

Modification history

2026-03-10 16:35
Mathlib/Geometry/Manifold/IsManifold/Basic.lean
feat: mfderiv_smul (#34263) …
Added NormedSpace.fromTangentSpaceView on Github →