mathlib
869cb328 - chore(measure_theory/probability_mass_function): Refactor the `pmf` file into a definitions file and a constructions file (#10298)

Commit

4 years ago

chore(measure_theory/probability_mass_function): Refactor the `pmf` file into a definitions file and a constructions file (#10298) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author

dtumad

Parents

a7e38a03

mathlib 869cb328 - chore(measure_theory/probability_mass_function): Refactor the `pmf` file into a definitions file and a constructions file (#10298)

mathlib
869cb328 - chore(measure_theory/probability_mass_function): Refactor the `pmf` file into a definitions file and a constructions file (#10298)