Def SchwartzMap.mkCLM

Modification history

2025-09-30 20:08
Mathlib/Analysis/Distribution/SchwartzSpace.lean
chore(Analysis/Distribution/SchwartzMap): correct a definition and add two lemmas (#29818) …
Modified SchwartzMap.mkCLMView on Github →
2023-06-19 04:18
Mathlib/Analysis/SchwartzSpace.lean
feat: port Analysis.SchwartzSpace (#4762)
Added SchwartzMap.mkCLMView on Github →