Theorem ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft

Modification history

2025-10-15 07:25
Mathlib/Probability/Independence/Conditional.lean
chore: fix the lemma name `condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight` (#30545) …
Deleted ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeftView on Github →
2025-10-02 14:28
Mathlib/Probability/Independence/Conditional.lean
feat(Probability): characterize conditional independence with conditional distributions (#30024) …
Added ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeftView on Github →