Theorem Measure.exists_hasLaw

Modification history

2026-04-09 07:32
Mathlib/Probability/HasLawExists.lean
chore: fix namespace in `Measure.exists_hasLaw` (#37825)
Deleted Measure.exists_hasLawView on Github →
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 →