Theorem ProbabilityTheory.iIndepFun_iff_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) …

Modified ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀'View on Github →

2025-10-26 07:20

Mathlib/Probability/Independence/InfinitePi.lean

feat: independence and uncurrying (#30184) …

Modified ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀'View on Github →

2025-08-03 18:35

Mathlib/Probability/Independence/InfinitePi.lean

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

Added ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀'View on Github →