Theorem ProbabilityTheory.indepFun_prod

Modification history

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