Theorem SchwartzMap.smulLeftCLM_const

Modification history

2026-01-13 18:40

Mathlib/Analysis/Distribution/SchwartzSpace.lean

feat(Analysis/SchwartzSpace): additional lemmas for `smulLeftCLM` (#33741) …

Modified SchwartzMap.smulLeftCLM_const View on Github →

2025-12-30 18:05

Mathlib/Analysis/Distribution/SchwartzSpace.lean

feat(Analysis/TemperedDistribution): multiplication with temperate growth functions (#32769) …

Added SchwartzMap.smulLeftCLM_const View on Github →