Theorem MDifferentiableAt.prodMap

Modification history

2026-03-05 11:23

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

chore(Geometry/Manifold/MFDeriv/SpecificFunctions): golf using custom… (#36009) …

Modified MDifferentiableAt.prodMap View on Github →

2025-04-19 07:34

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

chore(*): rename `Prod.map` lemmas (#24189) …

Added MDifferentiableAt.prodMap View on Github →