Theorem ProbabilityTheory.indepFun_iff_hasLaw_prodMk_prod

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.indepFun_iff_hasLaw_prodMk_prodView on Github →