Theorem TemperedDistribution.smulLeftCLM_compL_smulLeftCLM

Modification history

2025-12-30 18:05

Mathlib/Analysis/Distribution/TemperedDistribution.lean

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

Added TemperedDistribution.smulLeftCLM_compL_smulLeftCLM View on Github →