Mathlib Changelog
v4
Changelog
About
Github
Theorem
ProbabilityTheory.IndepFun.integral_fun_mul_eq_mul_integral
Modification history
2025-08-06 17:32
Mathlib/Probability/Independence/Integration.lean
feat: integral of product of indepent random variables (#27986) …
Added
ProbabilityTheory.IndepFun.integral_fun_mul_eq_mul_integral
View on Github →