Theorem MDifferentiableWithinAt.congr'

Modification history

2026-07-17 10:49

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

chore(Geometry/Manifold/MFDeriv/Basic): use custom elaborators (#40803) …

Modified MDifferentiableWithinAt.congr'View on Github →

2025-09-27 12:35

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

feat: `finsum` and locally finite sums of differentiable sections are differentiable (#29686) …

Added MDifferentiableWithinAt.congr'View on Github →