Commit 2025-04-03 07:54 38125904

View on Github →

feat(SetIntegral): add versions of integral_withDensity_eq_integral_smul (#23619)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem integral_withDensity_eq_integral_toReal_smul

added theorem integral_withDensity_eq_integral_toReal_smul₀

added theorem setIntegral_withDensity_eq_setIntegral_toReal_smul'

added theorem setIntegral_withDensity_eq_setIntegral_toReal_smul

added theorem setIntegral_withDensity_eq_setIntegral_toReal_smul₀'

added theorem setIntegral_withDensity_eq_setIntegral_toReal_smul₀