Def MeasureTheory.Measure.toTemperedDistribution

Modification history

2025-12-12 00:57

Mathlib/Analysis/Distribution/TemperedDistribution.lean

feat(Analysis/Distribution): definition of tempered distributions (#31757) …

Added MeasureTheory.Measure.toTemperedDistribution View on Github →