Theorem HasMFDerivWithinAt.prodMap

Modification history

2025-10-29 00:03

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

feat: add mfderiv_prod and mfderiv_prodMap (#29589) …

Added HasMFDerivWithinAt.prodMap View on Github →