Def Distribution.mapCLM

Modification history

2026-01-26 23:03

Mathlib/Analysis/Distribution/Distribution.lean

chore: bump toolchain to v4.28.0-rc1 (#34436) …

Deleted Distribution.mapCLM View on Github →

2025-12-09 20:06

Mathlib/Analysis/Distribution/Distribution.lean

feat: define the space of distributions (#32353)

Added Distribution.mapCLM View on Github →