Theorem ProbabilityTheory.Kernel.prod_prodMkRight_comp_deterministic_prod

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_prodMkRight_comp_deterministic_prodView on Github →