Theorem ProbabilityTheory.iIndepFun.hasLaw_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.hasLaw_piView on Github →