Theorem MDifferentiable.prodMap

Modification history

2026-05-16 04:19

MathlibTest/FunPropMinimal.lean

feat(fun_prop): allow fun_prop to call discharger on ModelWithCorners (#39226) …

Added MDifferentiable.prodMap View on Github →

2026-03-05 11:23

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

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

Modified MDifferentiable.prodMap View on Github →

2025-04-19 07:34

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

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

Added MDifferentiable.prodMap View on Github →