Commit 2025-12-09 20:06 806884d1

View on Github →

feat: define the space of distributions (#32353)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Distribution/Distribution.lean

added def Distribution.mapCLM

added theorem Distribution.mapCLM_apply

Modified docs/references.bib