Theorem ContDiffMapSupportedIn.fderivLM_eq_of_scalars

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