Theorem MDifferentiableOn.mdifferentiableAt

Modification history

2026-07-17 10:49
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
chore(Geometry/Manifold/MFDeriv/Basic): use custom elaborators (#40803) …
Modified MDifferentiableOn.mdifferentiableAtView on Github →
2023-06-27 07:44
Mathlib/Geometry/Manifold/MFDeriv.lean
feat: add `MDifferentiableOn.mdifferentiableAt` (#5510)
Added MDifferentiableOn.mdifferentiableAtView on Github →