Theorem ProbabilityTheory.iIndepFun.hasLaw_infinitePi

Modification history

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