Theorem TestFunction.coe_ofSupportedInLM

Modification history

2025-12-03 17:53
Mathlib/Analysis/Distribution/TestFunction.lean
feat: coercion to bounded continuous functions as a CLM on TestFunction (#32228) …
Deleted TestFunction.coe_ofSupportedInLMView on Github →
2025-12-01 09:11
Mathlib/Analysis/Distribution/TestFunction.lean
feat: endow test functions with the natural LF topology (#31806) …
Added TestFunction.coe_ofSupportedInLMView on Github →