Commit 2026-03-05 10:25 bbd1294f

View on Github →

chore(Geometry/Manifold/ContMDiffMFDeriv): golf using custom elaborators (#36008)

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

modified theorem ContMDiff.contMDiff_tangentMap

modified theorem ContMDiff.continuous_tangentMap

modified theorem ContMDiffAt.mfderiv_const

modified theorem ContMDiffOn.continuousOn_tangentMapWithin