Theorem ContDiffMapSupportedIn.fderivLM_apply_of_gt

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_gt View on Github →