Theorem MeasureTheory.Measure.ofMultiset_apply_singleton

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_apply_singletonView on Github →