Theorem ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map

Modification history

2025-03-29 13:22
Mathlib/Probability/Independence/Basic.lean
feat(Probability/Independence/Basic): upstream `iIndepFun_iff_pi_map_eq_map` from PFR (#23418) …
Added ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_mapView on Github →