Zulip Chat Archive
Stream: general
Topic: moving pmf to probability
Jason KY. (Jul 19 2022 at 11:59):
IIRC the reason why probability_mass_function exists in measure_theory instead of probability is only historical. Should we move that folder to probability now or is there a good reason why it's still placed there?
Johan Commelin (Jul 19 2022 at 11:59):
sgtm
Jason KY. (Jul 19 2022 at 12:04):
Last updated: Dec 20 2023 at 11:08 UTC