Theorem SchwartzMap.smulLeftCLM_real_smul

Modification history

2026-01-13 18:40
Mathlib/Analysis/Distribution/SchwartzSpace.lean
feat(Analysis/SchwartzSpace): additional lemmas for `smulLeftCLM` (#33741) …
Added SchwartzMap.smulLeftCLM_real_smulView on Github →