Theorem HasMFDerivWithinAt.prodMk

Modification history

2025-09-28 11:30

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

chore: move differentiability results about products to SpecificFunction (#30049) …

Modified HasMFDerivWithinAt.prodMk View on Github →

2025-09-01 07:30

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

feat(Geometry/Manifold/MFDeriv): HasMFDerivAt.prodMk (#29130) …

Added HasMFDerivWithinAt.prodMk View on Github →