Theorem HasMFDerivAt.prodMk

Modification history

2025-09-28 11:30
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
chore: move differentiability results about products to SpecificFunction (#30049) …
Modified HasMFDerivAt.prodMkView on Github →
2025-09-01 07:30
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
feat(Geometry/Manifold/MFDeriv): HasMFDerivAt.prodMk (#29130) …
Added HasMFDerivAt.prodMkView on Github →