Commit 2024-10-08 15:34 ae1fbb56

View on Github →

chore(MeasureTheory/Group/Arithmetic): tag more lemmas with fun_prop (#17304) ... and rewrite Measurable.mul' and Measurable.div' to be in compositional form From PFR

Estimated changes

modified theorem AEMeasurable.smul
modified theorem AEMeasurable.smul_const
modified theorem Finset.measurable_prod'
modified theorem Measurable.const_smul'
modified theorem Measurable.div'
modified theorem Measurable.mul'
added theorem Measurable.smul'
modified theorem Measurable.smul
modified theorem Measurable.smul_const
modified theorem Measurable.of_discrete