Theorem ProbabilityTheory.exists_iid

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_iidView on Github →