Theorem ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map

feat: add an alias for the forward direction of `indepFun_iff_map_prod_eq_prod_map_map` (#39767) …

feat: random variables are independent iff their joint distribution is the product measure (#26265) …