Theorem mdifferentiableOn_empty

Modification history

2026-07-17 10:49
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
chore(Geometry/Manifold/MFDeriv/Basic): use custom elaborators (#40803) …
Modified mdifferentiableOn_emptyView on Github →
2025-11-12 11:33
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
feat: add contMDiffOn_empty and friends (#31542) …
Added mdifferentiableOn_emptyView on Github →