Commit 2026-04-09 07:32 91b2017b

View on Github →

chore: fix namespace in Measure.exists_hasLaw (#37825)

Estimated changes

Modified Mathlib/Probability/HasLawExists.lean

deleted theorem Measure.exists_hasLaw

added theorem MeasureTheory.Measure.exists_hasLaw