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_prod₀View on Github →