Theorem ContDiffMapSupportedIn.fderivLM_apply_of_le

Modification history

2026-03-10 20:55

Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n (#30240) …

Added ContDiffMapSupportedIn.fderivLM_apply_of_le View on Github →