Def PMF.ofFinset

Modification history

2024-05-27 08:32

Mathlib/Probability/ProbabilityMassFunction/Constructions.lean

chore: Use the new `∑ i ∈ s, f i` notation (#13209) …

Modified PMF.ofFinset View on Github →

2023-10-06 14:17

Mathlib/Probability/ProbabilityMassFunction/Constructions.lean

chore(Probability): rename `Pmf` to `PMF` (#7542) …

Added PMF.ofFinset View on Github →