Theorem PMF.ofMultiset_apply_of_notMem

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) …
Deleted PMF.ofMultiset_apply_of_notMemView on Github →
2025-05-25 12:30
Mathlib/Probability/Distributions/Uniform.lean
chore(*): not_mem/nmem -> notMem (#25159)
Added PMF.ofMultiset_apply_of_notMemView on Github →