Commit 2026-05-26 05:50 f9900a34

feat: add an alias for the forward direction of indepFun_iff_map_prod_eq_prod_map_map (#39767) When assuming hXY : IndepFun X Y P, if one wants to rewrite P.map (fun w => (X w, Y w)) = (P.map X).prod (P.map Y), one has to use ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map, which is an iff with side-condition so is not convenient. We thus introduce an alias for this direction. We do the same for the iIndepFun version, removing the unnecessary IsProbabilityMeasure hypothesis there. We do the same in the infinitePi case too.