Theorem ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map

Modification history

2023-10-31 15:03
Mathlib/Probability/Independence/Basic.lean
feat(Probability/Density): Random variables are independent iff joint density is product (#8026) …
Added ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_mapView on Github →