Theorem ProbabilityTheory.iIndepFun_pi

Modification history

2025-08-07 07:54
Mathlib/Probability/Independence/Basic.lean
feat: random variables on separate spaces are independent (#27984) …
Added ProbabilityTheory.iIndepFun_piView on Github →