Commit 2026-03-10 19:08 bd534f1e

View on Github →

chore(Geometry/Manifold/MFDeriv/NormedSpace): use custom elaborators … (#36449) …at scale

Estimated changes

Modified Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

modified theorem Differentiable.comp_mdifferentiable

modified theorem Differentiable.comp_mdifferentiableAt

modified theorem DifferentiableAt.comp_mdifferentiableAt

modified theorem DifferentiableAt.comp_mdifferentiableWithinAt

modified theorem MDifferentiable.clm_postcomp

modified theorem MDifferentiable.clm_precomp

modified theorem MDifferentiable.smul

modified theorem MDifferentiableAt.clm_postcomp

modified theorem MDifferentiableAt.smul

modified theorem MDifferentiableOn.clm_precomp

modified theorem MDifferentiableOn.smul

modified theorem MDifferentiableWithinAt.cle_arrowCongr

modified theorem MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm