Theorem ProbabilityTheory.iIndepFun_iff_hasLaw_Pi_infinitePi

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_hasLaw_Pi_infinitePiView on Github →
2026-04-24 08:11
Mathlib/Probability/Independence/InfinitePi.lean
feat: the law of independent random variables is the product of their laws (#37830)
Added ProbabilityTheory.iIndepFun_iff_hasLaw_Pi_infinitePiView on Github →