Theorem ProbabilityTheory.iIndepFun.map_fun_eq_pi_map

Modification history

2026-05-26 05:50
Mathlib/Probability/Independence/Basic.lean
feat: add an alias for the forward direction of `indepFun_iff_map_prod_eq_prod_map_map` (#39767) …
Added ProbabilityTheory.iIndepFun.map_fun_eq_pi_mapView on Github →