Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-16 08:26
f38babea
View on Github →
feat:
comap
of a finite measure along a measurable equiv is finite (
#17639
) From PFR
Estimated changes
Modified
Mathlib/MeasureTheory/Measure/MeasureSpace.lean
added
theorem
MeasureTheory.Measure.nonempty_of_neZero
Modified
Mathlib/MeasureTheory/Measure/Typeclasses.lean