Commit 2023-05-10 08:59 bde5a1dc

View on Github →

feat: port MeasureTheory.Group.Arithmetic (#3823)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/Arithmetic.lean

added theorem AEMeasurable.const_div

added theorem AEMeasurable.const_mul

added theorem AEMeasurable.const_pow

added theorem AEMeasurable.const_smul'

added theorem AEMeasurable.const_smul

added theorem AEMeasurable.div'

added theorem AEMeasurable.div

added theorem AEMeasurable.div_const

added theorem AEMeasurable.inv

added theorem AEMeasurable.mul'

added theorem AEMeasurable.mul

added theorem AEMeasurable.mul_const

added theorem AEMeasurable.pow

added theorem AEMeasurable.pow_const

added theorem AEMeasurable.smul

added theorem AEMeasurable.smul_const

added theorem Finset.aemeasurable_prod'

added theorem Finset.aemeasurable_prod

added theorem Finset.measurable_prod'

added theorem Finset.measurable_prod

added theorem List.aemeasurable_prod'

added theorem List.aemeasurable_prod

added theorem List.measurable_prod'

added theorem List.measurable_prod

added theorem Measurable.const_div

added theorem Measurable.const_mul

added theorem Measurable.const_pow

added theorem Measurable.const_smul'

added theorem Measurable.const_smul

added theorem Measurable.div'

added theorem Measurable.div

added theorem Measurable.div_const

added theorem Measurable.inv

added theorem Measurable.mul'

added theorem Measurable.mul

added theorem Measurable.mul_const

added theorem Measurable.pow

added theorem Measurable.pow_const

added theorem Measurable.smul

added theorem Measurable.smul_const

added theorem MeasurableSet.inv

added theorem Multiset.aemeasurable_prod'

added theorem Multiset.aemeasurable_prod

added theorem Multiset.measurable_prod'

added theorem Multiset.measurable_prod

added theorem ae_eq_trim_of_measurable

added theorem aemeasurable_const_smul_iff

added theorem aemeasurable_const_smul_iff₀

added theorem aemeasurable_inv_iff

added theorem aemeasurable_inv_iff₀

added theorem measurableSet_eq_fun

added theorem measurableSet_eq_fun_of_countable

added theorem measurable_const_smul_iff

added theorem measurable_const_smul_iff₀

added theorem measurable_div_const'

added theorem measurable_inv_iff

added theorem measurable_inv_iff₀

added theorem measurable_mul_op

added theorem measurable_mul_unop

added theorem nullMeasurableSet_eq_fun