Def SchwartzMap.bilinLeftCLM

Modification history

2024-12-10 16:45

Mathlib/Analysis/Distribution/SchwartzSpace.lean

feat(Analysis/Distribution): generalize linearity of SchwartzMap.bilinLeftCLM (#19823) …

Modified SchwartzMap.bilinLeftCLM View on Github →

2023-06-19 04:18

Mathlib/Analysis/SchwartzSpace.lean

feat: port Analysis.SchwartzSpace (#4762)

Added SchwartzMap.bilinLeftCLM View on Github →