Theorem ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight

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) …
Added ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRightView on Github →