Theorem ProbabilityTheory.iIndepFun.map_fun_eq_infinitePi_map

Modification history

2026-05-26 05:50
Mathlib/Probability/Independence/InfinitePi.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_infinitePi_mapView on Github →