Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 15:04 4d79d5fe

View on Github →

chore(measure_theory/group/arithmetic): use implicit argument for measurable_space (#11205) The measurable_space argument is inferred from other arguments (like measurable f or a measure for example) instead of being a type class. This ensures that the lemmas are usable without @ when several measurable space structures are used for the same type. Also use more variables.

Estimated changes

modified theorem ae_measurable.inner
modified theorem measurable.inner
modified theorem ae_measurable.const_div
modified theorem ae_measurable.const_mul
modified theorem ae_measurable.const_pow
modified theorem ae_measurable.const_smul'
modified theorem ae_measurable.const_smul
modified theorem ae_measurable.div'
modified theorem ae_measurable.div
modified theorem ae_measurable.div_const
modified theorem ae_measurable.inv
modified theorem ae_measurable.mul'
modified theorem ae_measurable.mul
modified theorem ae_measurable.mul_const
modified theorem ae_measurable.pow
modified theorem ae_measurable.pow_const
modified theorem ae_measurable.smul_const
modified theorem finset.ae_measurable_prod'
modified theorem finset.ae_measurable_prod
modified theorem finset.measurable_prod'
modified theorem finset.measurable_prod
modified theorem list.ae_measurable_prod'
modified theorem list.ae_measurable_prod
modified theorem measurable.const_div
modified theorem measurable.const_mul
modified theorem measurable.const_pow
modified theorem measurable.const_smul'
modified theorem measurable.const_smul
modified theorem measurable.div'
modified theorem measurable.div
modified theorem measurable.div_const
modified theorem measurable.inv
modified theorem measurable.mul'
modified theorem measurable.mul
modified theorem measurable.mul_const
modified theorem measurable.pow
modified theorem measurable.pow_const
modified theorem measurable.smul
modified theorem measurable.smul_const
modified theorem measurable_set_eq_fun
modified theorem multiset.ae_measurable_prod