Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-16 14:07
d3d1be67
View on Github →
feat: post-composing independent random variables (
#17811
) From PFR
Estimated changes
Modified
Mathlib/Probability/Independence/Basic.lean
Modified
Mathlib/Probability/Independence/Kernel.lean
added
theorem
ProbabilityTheory.Kernel.iIndepFun.comp