Theorem ProbabilityTheory.iIndepFun_iff_hasLaw_pi_pi

Modification history

2026-04-24 08:11
Mathlib/Probability/HasLaw.lean
feat: the law of independent random variables is the product of their laws (#37830)
Added ProbabilityTheory.iIndepFun_iff_hasLaw_pi_piView on Github →