Theorem ContDiffMapSupportedIn.monoLM_eq_of_scalars

Modification history

2026-03-18 18:00
Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
feat: monotonicity of D^n(U) in n and in U as CLMs (#32401)
Added ContDiffMapSupportedIn.monoLM_eq_of_scalarsView on Github →