Theorem ContDiffMapSupportedIn.seminorm_fderivLM_top

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