feat: port Probability.ProbabilityMassFunction.Basic (#3865)

leanprover-community · May 9, 2023 · 68b21e1 · 68b21e1
1 parent 98de133
commit 68b21e1
Show file tree

Hide file tree

Showing 2 changed files with 400 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1691,6 +1691,7 @@ import Mathlib.Order.WellFoundedSet
 import Mathlib.Order.WithBot
 import Mathlib.Order.Zorn
 import Mathlib.Order.ZornAtoms
+import Mathlib.Probability.ProbabilityMassFunction.Basic
 import Mathlib.RepresentationTheory.Maschke
 import Mathlib.RingTheory.Adjoin.Basic
 import Mathlib.RingTheory.Adjoin.Fg