feat: port Probability.Kernel.Basic (#4879)

leanprover-community · Jun 9, 2023 · 4b23323 · 4b23323
1 parent 2ca5e13
commit 4b23323
Show file tree

Hide file tree

Showing 2 changed files with 678 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2297,6 +2297,7 @@ import Mathlib.Probability.ConditionalProbability
 import Mathlib.Probability.Independence.Basic
 import Mathlib.Probability.Independence.ZeroOne
 import Mathlib.Probability.Integration
+import Mathlib.Probability.Kernel.Basic
 import Mathlib.Probability.ProbabilityMassFunction.Basic
 import Mathlib.Probability.ProbabilityMassFunction.Constructions
 import Mathlib.Probability.ProbabilityMassFunction.Monad