Commit 2023-08-24 17:13 1239d77c

View on Github →

feat: Pmf.binomial (#6425) Inspired by a file by @pfaffelh

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/ProbabilityMassFunction/Binomial.lean

added def Pmf.binomial

added theorem Pmf.binomial_apply

added theorem Pmf.binomial_apply_self

added theorem Pmf.binomial_apply_zero

added theorem Pmf.binomial_one_eq_bernoulli