Commit 2025-05-20 14:57 1657f90a

View on Github →

feat: Measure.comap_smul (#25052) comap f (c • μ) = c • comap f μ

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Comap.lean

added theorem MeasureTheory.Measure.comap_smul

added theorem MeasureTheory.Measure.comap_undef

Modified Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean

added theorem MeasureTheory.NullMeasurableSet.smul_measure

added theorem MeasureTheory.nullMeasurableSet_smul_measure_iff