Commit 2026-01-27 20:36 6ce5fb97
View on Github →feat(Probability): UniformOn_univ_instIsProbabilityMeasure (#33613)
It is convenient to have an instance of IsProbabilityMeasure on a uniform distribution on .univ (to avoid the need for haveI statements). There is perhaps an argument for abbrev uniform := uniformOn (.univ : Set Ω) but I have not implemented this in this PR.