Theorem fromTangentSpace_mfderiv_smul_apply'

Modification history

2026-03-10 16:35
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: mfderiv_smul (#34263) …
Added fromTangentSpace_mfderiv_smul_apply'View on Github →