Commit 2026-04-24 08:11 7d585981

View on Github →

feat: the law of independent random variables is the product of their laws (#37830)

Estimated changes

Modified Mathlib/Probability/HasLaw.lean

added theorem ProbabilityTheory.iIndepFun.hasLaw_pi

added theorem ProbabilityTheory.iIndepFun_iff_hasLaw_pi_pi

added theorem ProbabilityTheory.indepFun_iff_hasLaw_prodMk_prod

Modified Mathlib/Probability/Independence/InfinitePi.lean

added theorem ProbabilityTheory.iIndepFun.hasLaw_infinitePi

added theorem ProbabilityTheory.iIndepFun_iff_hasLaw_Pi_infinitePi