Theorem ProbabilityTheory.iIndepFun_congr

Modification history

2025-08-03 18:35
Mathlib/Probability/Independence/Basic.lean
feat: random variables are independent iff their joint distribution is the product measure (#26265) …
Added ProbabilityTheory.iIndepFun_congrView on Github →