Theorem ProbabilityTheory.Kernel.prod_prodMkLeft_comp_prod_deterministic

Modification history

2025-10-02 14:28
Mathlib/Probability/Kernel/Composition/Lemmas.lean
feat(Probability): characterize conditional independence with conditional distributions (#30024) …
Added ProbabilityTheory.Kernel.prod_prodMkLeft_comp_prod_deterministicView on Github →