Theorem SchwartzMap.sum_apply

Modification history

2026-06-10 10:42
Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
feat(Analysis/Distribution): use `Is*Apply` for `SchwartzMap` (#40447) …
Deleted SchwartzMap.sum_applyView on Github →
2026-01-13 18:40
Mathlib/Analysis/Distribution/SchwartzSpace.lean
feat(Analysis/SchwartzSpace): additional lemmas for `smulLeftCLM` (#33741) …
Added SchwartzMap.sum_applyView on Github →