Commit 2026-10-07 12:33 4e77f237

View on Github →

chore(Geometry/Manifold/ContMDiff/NormedSpace): use custom elaborators more (#44549)

Estimated changes

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

modified theorem ContMDiff.clm_postcomp

modified theorem ContMDiff.clm_precomp

modified theorem ContinuousLinearMap.contMDiff

modified theorem ContinuousLinearMap.contMDiffAt

modified theorem ContinuousLinearMap.contMDiffOn

modified theorem contMDiff_iff_contDiff