Def MeasureTheory.Measure.ofMultiset

Modification history

2026-10-05 07:41

Mathlib/Probability/Distributions/Uniform.lean

refactor(Probability/Distributions/Uniform): change uniformOfFinset and ofMultiset from PMF to Measure (#42909) …

Added MeasureTheory.Measure.ofMultiset View on Github →