Theorem ProbabilityTheory.exists_hasLaw_indepFun

Modification history

2025-10-08 08:14
Mathlib/Probability/HasLawExists.lean
feat(Probability): existence of independent random variables with a given sequence of distributions (#29959) …
Added ProbabilityTheory.exists_hasLaw_indepFunView on Github →