Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.isProbabilityMeasure_iff_real
Modification history
2025-12-14 14:45
Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean
feat: more API for FiniteMeasure and ProbabilityMeasure (#32784)
Added
MeasureTheory.isProbabilityMeasure_iff_real
View on Github →