Commit 2026-01-13 18:40 f3ee4921

View on Github →

feat(Analysis/SchwartzSpace): additional lemmas for smulLeftCLM (#33741) Add various lemmas for smulLeftCLM.

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

added theorem SchwartzMap.smulLeftCLM_add

modified theorem SchwartzMap.smulLeftCLM_const

added theorem SchwartzMap.smulLeftCLM_neg

added theorem SchwartzMap.smulLeftCLM_ofReal

added theorem SchwartzMap.smulLeftCLM_real_smul

added theorem SchwartzMap.smulLeftCLM_smul

added theorem SchwartzMap.smulLeftCLM_sub

added theorem SchwartzMap.smulLeftCLM_sum

added theorem SchwartzMap.sum_apply