Theorem Measure.exists_hasLaw

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